/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */
package alloy.transform.atomize;

import java.util.ArrayList;
import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.LinkedHashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Set;

import alloy.ast.ASTDepthFirstReplacer;
import alloy.ast.ArrowMultExpr;
import alloy.ast.BinaryExpr;
import alloy.ast.BinaryExprOp;
import alloy.ast.BinaryFormula;
import alloy.ast.BinaryIntExpr;
import alloy.ast.CardinalityExpr;
import alloy.ast.CheckCommand;
import alloy.ast.CompOp;
import alloy.ast.ComprehensionExpr;
import alloy.ast.Decl;
import alloy.ast.Decls;
import alloy.ast.ElemFormula;
import alloy.ast.ElemIntFormula;
import alloy.ast.EmptyExpr;
import alloy.ast.EmptyFormula;
import alloy.ast.EmptySetExpr;
import alloy.ast.Expr;
import alloy.ast.ExprCastIntExpr;
import alloy.ast.Fact;
import alloy.ast.FindCommand;
import alloy.ast.Formula;
import alloy.ast.FormulaSeq;
import alloy.ast.Formulas;
import alloy.ast.Id;
import alloy.ast.IdentityExpr;
import alloy.ast.IfThenElseExpr;
import alloy.ast.IntCompOp;
import alloy.ast.IntExpr;
import alloy.ast.IntExprCastExpr;
import alloy.ast.IntExprOp;
import alloy.ast.LeafExpr;
import alloy.ast.LeafId;
import alloy.ast.LiteralIntExpr;
import alloy.ast.LogicOp;
import alloy.ast.Multiplicity;
import alloy.ast.MultiplicityExpr;
import alloy.ast.Node;
import alloy.ast.Paragraph;
import alloy.ast.QualifiedName;
import alloy.ast.Qualifier;
import alloy.ast.Qualifiers;
import alloy.ast.QuantifiedExpr;
import alloy.ast.QuantifiedFormula;
import alloy.ast.Quantifier;
import alloy.ast.RunCommand;
import alloy.ast.Scope;
import alloy.ast.SetMultExpr;
import alloy.ast.SigExpr;
import alloy.ast.SigExprs;
import alloy.ast.SigmaExpr;
import alloy.ast.Signature;
import alloy.ast.Signatures;
import alloy.ast.SumIntExpr;
import alloy.ast.TypeScope;
import alloy.ast.UnaryExpr;
import alloy.ast.UnaryExprOp;
import alloy.ast.UniversalExpr;
import alloy.ast.VarCreator;
import alloy.ast.Variable;
import alloy.ast.VariableExpr;
import alloy.ast.Variables;
import alloy.semantic.LocalScope;
import alloy.semantic.SignatureReferenceCounter;
import alloy.transform.LeafIdMap;
import alloy.type.BasicType;
import alloy.type.RelationType;
import alloy.type.SigType;
import alloy.type.UnionType;
import alloy.util.Dbg;
import alloy.util.Msg;
import alloy.util.Params;

/**
 * Visitor for figuring out which are the atomized types and making the
 * necessary changes (and keeping track of the mappings for later
 * back-conversion).
 * 
 * The following constraints are explicitly added by the atomizer: 1.
 * Cardinality constraints on types when using the "difference" optimization for
 * inferring type scopes while determining the atomic types of a command. That
 * is, if A has subtypes A_1,...A_n, and all but one of those subtypes are
 * exactly scoped, the scope of the sole unscoped subtype A_k may be inferred by
 * subtraction. If A is exactly scoped, then A_k is as well, and the constraint
 * "#A_k = (number)" is added. 2. Cardinality constraints when subtypes are made
 * subsets. e.g. in the example above, if more than one of A_1,...,A_n are
 * unscoped, which forces A to be the atomic type, then A_1,...,A_n are
 * converted from subtypes to merely subsets of type A. In order to retain any
 * user-specified scopes on A_1,...,A_n, constraints like "#A_1<=(scope)" are
 * added.
 */
public class AtomizationVisitor extends ASTDepthFirstReplacer {

	private final CommandState info;

	/** separator used for remainder types */
	public static final String ATOMIZATION_SEPARATOR = "$";

	private TransientState transientState;

	/** for atomization debug println's */
	private final boolean DEBUG = false;

	// ************************************************************
	// State information kept in the visitor
	// includes information about what the atomic types are, etc.
	// this info can be encapsulated as an AtomizationInfo object
	// for storage in a command
	// *************************************************************

	// /** stores all Signatures in all modules */
	// private Set _allSigs = new LinkedHashSet();
	// // Important: storing _allSigs in AtomizationInfo fixed AtomizationBug4,
	// which was
	// // due to the fact that generateSubsetMappings couldn't run properly with
	// an
	// // empty _allSigs.
	//    
	// /** set of SigTypes that are selected as atomic */
	// private Set _atomicTypes;
	//    
	// /**
	// * Maps LeafId's of expressions (both in the atomized and original asts)
	// * back to their original forms. Expressions that got broken down
	// * in atomization will map to themselves.
	// */
	// private Map _atomizedIdToOldLeafExpr;
	//
	// /**
	// * stores the current _command being atomized
	// */
	// private Command _command;
	//    
	// /**
	// * A stringToType map that only contains new SigTypes created during
	// * atomization (i.e. remainder types).
	// */
	// private Map _createdStringToType = new LinkedHashMap();
	//
	// /** Current module's ModuleInfo */
	// private ModuleInfo _curModuleInfo;
	//
	// /**
	// * mapping of LeafId's for fields to their SigmaExpr replacements,
	// * if applicable
	// */
	// private Map _fieldIdToSigmaExpr;
	//
	// /** visitor that can be run to ensure that all LeafId's are set and
	// consistent */
	// private FixLeafIdsVisitor _fliv;
	//
	// /**
	// * mapping of LeafId's for SigExpr's to their SigmaExpr replacements
	// * (in place of SigExpr's for these SigTypes), if applicable
	// */
	// private Map _sigIdToSigmaExpr;
	//
	// /**
	// * a mapping from SigType's to their TypeScope's (if any)
	// * used to determine if it was exact
	// */
	// private Map _sigTypeToTypeScope;
	//
	// /** mapping from subtype its unique atomic supertype */
	// private Map _subToAtomic;
	//
	// /** mapping from supertype to set of atomic types that partition it */
	// private Map _superToAtomic;
	//
	// /**
	// * mapping of LeafId's for VariableExpr's to their SigmaExpr replacements
	// * currently used exclusively for skolem constants.
	// */
	// private Map _varIdToSigmaExpr;

	// ***********************************************************
	// utility functions
	// ************************************************************

	/**
	 * create a String with the fully qualified names of all signatures
	 * mentioned in a SigExpr, for use in matching to a type
	 */
	private String _fullyQualifiedTypeString(SigExpr sigExpr_,
			List typeStrings_, boolean nested_) {
		String sigString = sigExpr_.nodeString();

		// check for "int"
		/**
		 * if (typeStrings_.contains(sigExpr_.nodeString())) { return
		 * sigExpr_.nodeString(); }
		 */
		if (sigExpr_.nodeString().equals("int")) {
			return sigExpr_.nodeString();
		}

		// construct string recursively
		QualifiedName baseName = sigExpr_.getSig();
		if (baseName.hasEmptyPath()) { // unqualified name
			Paragraph sigPara = info._command.moduleInfo.getSignature(baseName,
					"set scope");
			if (sigPara == null) {
				return null;
			} else {
				baseName = ((Signature) sigPara).getName();
			}
		}

		return baseName.nodeString();
	}

	/**
	 * returns a List of RelationTypes equivalent to the input type in its
	 * atomized form note that a UnionType was not returned because there's code
	 * there that automatically "normalizes" types (so, if A1 and A2 which
	 * extend A were atomic types, it'd merge A1 and A2 if they both appear,
	 * which is precisely what we don't want here)
	 */
	private List atomizeType(UnionType type) {
		Dbg.chk(type, "atomizeType called on null type");
		List relTypes = new ArrayList();

		for (Iterator relTypeIter = type.getTypeIter(); relTypeIter.hasNext();) {
			RelationType relType = (RelationType) relTypeIter.next();
			List columns = new ArrayList(relType.arity());
			for (Iterator basTypeIter = relType.getTypeIter(); basTypeIter
					.hasNext();) {
				BasicType basType = (BasicType) basTypeIter.next();
				// System.out.println(" column: " + basType);
				List typesInColumn = new ArrayList();
				if (basType instanceof SigType) {
					// look it up and see if it expands into anything.
					if (info._superToAtomic.containsKey(basType)) {
						// System.out.println(" replacing with: " +
						// _superToAtomic.get(basType));
						typesInColumn.addAll((Set) info._superToAtomic
								.get(basType));
					} else if (info._subToAtomic.containsKey(basType)) {
						// change the type to the atomic type
						typesInColumn.add(info._subToAtomic.get(basType));
					} else {
						// no change needed
						typesInColumn.add(basType);
					}

				} else {
					// must be an IntType or EmptyType. Won't be expanded in
					// atomization
					typesInColumn.add(basType);
				}
				columns.add(typesInColumn);
			}

			// now generate the list of RelationType's from relType
			int[] indices = new int[columns.size()];
			// initialize indices
			for (int i = 0; i < indices.length; i++) {
				indices[i] = 0;
			}

			do {
				List basTypes = new ArrayList(indices.length);
				for (int i = 0; i < indices.length; i++) {
					BasicType basType = (BasicType) ((List) columns.get(i))
							.get(indices[i]);
					basTypes.add(basType);
				}
				RelationType newRelType = new RelationType(basTypes);
				if (!relTypes.contains(newRelType))
					relTypes.add(newRelType);
			} while (increment(indices, columns, indices.length - 1));

		}

		Dbg.chk(relTypes.size() >= 1,
				"no atomic RelationTypes were generated from this UnionType: "
						+ type);

		return relTypes;
	}

	private void consolePrintResults() {
		System.out.println("atomic types: [");
		for (Iterator aIter = info._atomicTypes.iterator(); aIter.hasNext();) {
			SigType sig = (SigType) aIter.next();
			System.out.println("  " + sig + ", id: "
					+ sig.getSignature().getLeafId() + ", scope: "
					+ getScope(sig));
		}
		System.out.println("]");

		System.out.println("\nsupertype mappings: \n" + info._superToAtomic);
		System.out.println("\nsubtype mappings: \n" + info._subToAtomic);
		System.out.println("\nsigExpr replacements: \n"
				+ info._sigIdToSigmaExpr);
		System.out.println("\nvarExpr replacements: \n"
				+ info._fieldIdToSigmaExpr);
		System.out.println("\nformula for " + info._command);
		System.out.println(((FindCommand) info._command).formula.pp());
		// System.out.println(((FindCommand)_command).formula.nodeString());
	}

	/**
	 * returns a name of the form origName$type_1$type_2$...$type_n
	 * 
	 * @param origName
	 *            original name of the field
	 * @param type
	 *            the RelationType from which the mangled name is created
	 * @return
	 */
	private String createMangledFieldName(String origName, RelationType type) {
		StringBuffer ret = new StringBuffer(origName);

		Iterator typeIter = type.getTypeIter();
		/*
		 * BasicType basType = (BasicType)typeIter.next();
		 * ret.append(basType.toString());
		 */

		while (typeIter.hasNext()) {
			ret.append(ATOMIZATION_SEPARATOR);
			ret.append(((BasicType) typeIter.next()).toString());
		}

		return ret.toString();
	}

	// ************************************************************
	// functions for traversing the AST and figuring out how
	// to atomize
	// ************************************************************

	/**
	 * Determines which types to make atomic, and then calls the appropriate
	 * methods to create LeafId mappings from old leaves to equivalent
	 * SigmaExpr's.
	 * 
	 * (1) traverses type hierarchy to determine atomic types, using scoping and
	 * type checker information to make the decision. Remainder types are
	 * created in the process. (2) adds "exact" cardinality constraints in cases
	 * for which these optimizations apply (3) creates mappings from (i)
	 * supertypes of atomic types to their equivalents as unions of atomic
	 * types, (ii) subtypes of atomic types to subsets, (iii) subsets and fields
	 * of all types.
	 */
	private void determineAtomicTypesAndRelations() {

		/*
		 * Important note about how remainder types are handled:
		 * 
		 * If type A requires a subtype A$ in any command's scope, then such an
		 * A$ will be generated. Note that this generation produces a permanent
		 * change in SigType, so that SigType.getSubtypes() for A will always
		 * include A$, even for commands that don't need a remainder type A$.
		 * For uniformity, however, information about remainder types are stored
		 * in every command as they become available. The types just won't be
		 * used if they are not needed.
		 * 
		 * _createdStringToType makes sure that AtomizationVisitor knows about
		 * all the remainder types that have been put into SigType by atomizing
		 * previous commands; therefore, it must be stored in AtomizationInfo.
		 */
		info._command.stringToType
				.putAll(AtomizationState.state._createdStringToType);

		// for each of those remainders, need to make sure some cleanup work is
		// done
		// (1) need to map remainder to its original supertype
		for (Iterator remTypes = AtomizationState.state._createdStringToType
				.values().iterator(); remTypes.hasNext();) {
			SigType remType = (SigType) remTypes.next();
			SigType origType = remType.getSuperType();
			Dbg.chk(origType);
			info._atomizedIdToOldLeafExpr.put(remType.getSignature()
					.getLeafId(), origType.getSignature().toSigExpr());
		}

		Set frontierTypes = new LinkedHashSet();

		Set newExactTypes = new LinkedHashSet(); // set of SigType's that we
													// made exact

		// initialize typescope info

		Scope scope = info._command.getScope();
		Iterator scopeIter = scope.getTypeScopes().getTypeScopeIter();

		// this line should be redundant ...
		Dbg.chk(info._sigTypeToTypeScope.size() == 0);
		info._sigTypeToTypeScope.clear(); // = new LinkedHashMap();

		while (scopeIter.hasNext()) {
			TypeScope tscope = (TypeScope) scopeIter.next();

			String typeName = _fullyQualifiedTypeString(tscope.getSigExpr(),
					new ArrayList(SigType.getSigTypeStrings()), false);

			SigType stype = SigType.getSigTypeForString(typeName);
			info._sigTypeToTypeScope.put(stype, tscope);
		}

		// determine starting frontier types
		// note: with the current implementation, the set of starting frontier
		// types
		// always consists of just univ.
		for (Iterator typesIter = SigType.getSigTypes().iterator(); typesIter
				.hasNext();) {
			SigType sig = (SigType) typesIter.next();
			if (sig.getSuperType() == null) {
				// top-level types are added to the set of frontier types
				frontierTypes.add(sig);
				Dbg.chk(getScope(sig) >= 0, "top-level type scope not set: "
						+ sig);
			}
		}

		System.out.println(info._command.moduleInfo);
		Set closedTypes = info._command.moduleInfo.getClosedTypes();
		SignatureReferenceCounter.CountTree sigRefCountTree = info._command.moduleInfo
				.getSigRefCountTree();

		/*
		 * The strategy for determining atomic types is as follows: (1)
		 * initialize a set of "frontier types" to the top-level types (because
		 * we now have a univ type, the frontier types set will initially
		 * contain only this type) (2) for every frontier type, check if it's a
		 * closed type. If so, make the frontier type atomic (and remove the
		 * type from the set of frontier types). (3) if the frontier type is not
		 * closed, check if it's abstract. If not, make it so and create a
		 * remainder type. (4) for every abstract frontier type, check if all
		 * its subtypes are scoped. If so, then add its subtypes to and remove
		 * itself from the set of frontier types. (5) if, for an abstract
		 * frontier type, all but one of its subtypes are scoped, and each of
		 * those scopes are exact, then we can infer the scope on the sole
		 * unscoped subtype, and we can apply (4). (6) if (4) or (5) don't
		 * apply, then make the frontier type atomic (and remove it from the set
		 * of frontier types).
		 * 
		 * (an implicit invariant is that at any point, every frontier type is
		 * scoped, and all frontier types together partition the universe)
		 * 
		 * HEURISTICS IN PLACE FOR PERFORMANCE: 1. TREAT SCOPES OF 1 as if they
		 * were unscoped, as an attempt to reduce the expression explosion that
		 * we're seeing in the beta. Do this unless you're looking at a
		 * top-level type (because you don't want univ to be atomic)
		 * 
		 * 2. treat types with zero references in fields (as determined in
		 * ModuleInfo.getSigRefCountTree()) as if they're unscoped, unless it's
		 * a top-level type.
		 */

		// if atomization is disabled, make top-level types (children of univ)
		// atomic.
		boolean disableAtomization = Params.glob.getBoolParam("MAIN",
				"disableAtomization", false);
		if (disableAtomization) {

			// univ should be only type there so far under the current semantics
			// of Alloy 3
			Dbg.chk(frontierTypes.size() == 1);

			SigType univType = (SigType) frontierTypes.iterator().next();
			frontierTypes.addAll(univType.getSubTypes());
			frontierTypes.remove(univType);

			// set the necessary vars for univ
			Signature univSig = univType.getSignature();
			// if this is not a remainder type (generated for atomization
			// purposes)
			// then map it to itself in _atomizedIdToOldLeafExpr
			if (!AtomizationState.state._createdStringToType
					.containsKey(univSig.getName().nodeString())) {
				SigExpr sigExpr = univSig.toSigExpr();
				info._atomizedIdToOldLeafExpr.put(univSig.getLeafId(), sigExpr);
			}

			for (Iterator ftIter = frontierTypes.iterator(); ftIter.hasNext();) {
				SigType type = (SigType) ftIter.next();

				Signature sig = type.getSignature();
				// if this is not a remainder type (generated for atomization
				// purposes)
				// then map it to itself in _atomizedIdToOldLeafExpr
				if (!AtomizationState.state._createdStringToType
						.containsKey(sig.getName().nodeString())) {
					SigExpr sigExpr = sig.toSigExpr();
					info._atomizedIdToOldLeafExpr.put(sig.getLeafId(), sigExpr);
				}

				makeTypeAtomic(type);
			}
		} else {
			// otherwise use the algorithm described above

			// used to keep track of whether or not we're still looking at top
			// level types
			int currentDepth = 0;

			// if true, treats types with scope of one as unscoped
			boolean useOneHeuristic = Params.glob.getBoolParam("MAIN",
					"oneAtomHeuristic", true);

			// if true, treats types with no references in field declarations as
			// unscoped
			boolean useSigRefHeuristic = Params.glob.getBoolParam("MAIN",
					"sigRefAtomHeuristic", true);

			while (!frontierTypes.isEmpty()) {
				Set newFrontierTypes = new LinkedHashSet();

				for (Iterator ftIter = frontierTypes.iterator(); ftIter
						.hasNext();) {
					SigType type = (SigType) ftIter.next();

					Signature sig = type.getSignature();

					// if this is not a remainder type (generated for
					// atomization purposes)
					// then map it to itself in _atomizedIdToOldLeafExpr
					if (!AtomizationState.state._createdStringToType
							.containsKey(sig.getName().nodeString())) {
						SigExpr sigExpr = sig.toSigExpr();
						info._atomizedIdToOldLeafExpr.put(sig.getLeafId(),
								sigExpr);
					}

					// If there's a transitive closure over this type in the
					// model, make it
					// atomic. No remainder type will be created for it.
					// Exception case--if the closed type is univ, let it go
					// because we can
					// desugar that
					if (closedTypes.contains(type) && currentDepth > 0) {
						makeTypeAtomic(type);
						continue;
					}

					// supertypes need to be abstract. If it isn't, make it so
					// and
					// create a "remainder type" containing all its atoms that
					// belong
					// to none of its original subtypes.
					if (!sig.isAbstract()
							&& !sig.getSigType().getSubTypes().isEmpty()) {
						String remainderNameString = sig.getName().getId()
								.nodeString()
								+ ATOMIZATION_SEPARATOR;
						String qualifiedRemainderNameString = sig.getName()
								.nodeString()
								+ ATOMIZATION_SEPARATOR;

						// System.out.println("making remainder:
						// "+remainderNameString);
						if (!AtomizationState.state._createdStringToType
								.containsKey(qualifiedRemainderNameString)) {
							QualifiedName name = new QualifiedName(sig
									.getLocation(), new Id(sig.getLocation(),
									remainderNameString), sig.getName()
									.getPath());

							SigExprs xtends = new SigExprs(sig.getLocation());
							xtends.addSigExpr(sig.toSigExpr());
							Signature remainder = new Signature(sig
									.getLocation(), name, xtends, sig
									.getSubsets(),
									new Decls(sig.getLocation()), new Fact(sig
											.getLocation(), new QualifiedName(
											sig.getLocation(), Id
													.generateId("Fact"), name
													.getPath()),
											new FormulaSeq(sig.getLocation(),
													new Formulas(sig
															.getLocation()))),
									Multiplicity.NONE, sig.isProduct(), true);
							remainder.setLeafIdMap(new LeafIdMap(sig
									.getLeafIdMap()));
							remainder.setParent(sig.getParent());
							remainder.setLeafId(new LeafId());
							remainder.annotate("remainder type for " + sig);

							info._atomizedIdToOldLeafExpr.put(remainder
									.getLeafId(), sig.toSigExpr());

							try {
								info._command.moduleInfo.addUsedParagraph(name,
										remainder);
							} catch (Exception e) {
								Dbg
										.fail("exception while trying to add signature in atomization: "
												+ remainder);
							}

							// so the type hierarchy knows of the remainder type
							// and creates
							// all the subtyping relationships
							remainder.setSigType(SigType
									.getGlobalSigType(remainder));
							AtomizationState.state._createdStringToType
									.put(qualifiedRemainderNameString, SigType
											.getGlobalSigType(remainder));

							sig.setAbstract(true);
						}
					}

					if (type.getSubTypes().isEmpty()) {
						// if it's a leaf, it's atomic
						makeTypeAtomic(type);
					} else {

						// figure out how many subtypes are unscoped, etc.
						int numUnscoped = 0;
						int sumOfScoped = 0;
						// we use the difference optimization only if all scopes
						// were exact

						// Note: TREAT SCOPES OF 1 as if they were unscoped, as
						// an attempt to reduce
						// the expression explosion that we're seeing in the
						// beta. Do this unless
						// you're looking at a top-level type (because you don't
						// want univ to be atomic).
						//
						// Also, treat types with zero references in fields (as
						// determined in ModuleInfo.getSigRefCountTree())
						// as if they're unscoped, unless it's a top-level type.
						boolean allExact = true;
						SigType unscopedSub = null;
						for (Iterator subTypes = type.getSubTypes().iterator(); subTypes
								.hasNext();) {
							SigType sub = (SigType) subTypes.next();
							int subtypeScope = getScope(sub);
							if (subtypeScope == -1
									|| (useOneHeuristic && subtypeScope == 1 && currentDepth > 0)
									|| (useSigRefHeuristic
											&& sigRefCountTree.getCount(sub) == 0 && currentDepth > 0)) {
								numUnscoped++;
								unscopedSub = sub;
							} else {
								TypeScope typescope = (TypeScope) info._sigTypeToTypeScope
										.get(sub);

								if (!sub.getSignature().getMult().equals(
										Multiplicity.ONE)
										&& (typescope == null || !typescope
												.isExact())) {
									allExact = false;
								}
								sumOfScoped += subtypeScope;
							}
						}

						// if all subtypes are scoped, move on down
						if (numUnscoped == 0) {
							newFrontierTypes.addAll(type.getSubTypes());
							// remove frontier type from exact set
							newExactTypes.remove(type);
							// remove it from the mapping for *scoped* types
							info._command.stringToType.remove(type);

						} else if (numUnscoped == 1 && allExact /*
																 * supertype
																 * doesn't need
																 * to be exact,
																 * however
																 */
						) {
							info._command.leafId2Scope.put(unscopedSub
									.getSignature().getLeafId(), new Integer(
									getScope(type) - sumOfScoped));

							newFrontierTypes.addAll(type.getSubTypes());

							// if supertype was also exact, remainder type must
							// be exact
							Multiplicity mult = type.getSignature().getMult();
							if (mult.equals(Multiplicity.ONE)
									|| (info._sigTypeToTypeScope.get(type) != null && ((TypeScope) info._sigTypeToTypeScope
											.get(type)).isExact())) {
								// so add exact constraint
								newExactTypes.add(unscopedSub);
							}

							// remove the now useless frontier type in case it
							// was made
							// exact earlier
							newExactTypes.remove(type);

							// remove it from the mapping for *scoped* types
							info._command.stringToType.remove(type);
						} else {
							// more than one unscoped subtype, make this atomic.
							makeTypeAtomic(type);
						}
					}
				}

				currentDepth++;
				frontierTypes = newFrontierTypes;
			}
		}

		// add constraints for exact scopes from difference optimization
		for (Iterator typesIter = newExactTypes.iterator(); typesIter.hasNext();) {
			SigType type = (SigType) typesIter.next();
			Formula cardFormula = new ElemIntFormula(info._command
					.getLocation(), new CardinalityExpr(info._command
					.getLocation(), type.getSignature().toSigExpr()),
					IntCompOp.INT_EQUALS, new LiteralIntExpr(info._command
							.getLocation(), getScope(type)));
			Formulas formulas = ((FormulaSeq) ((FindCommand) info._command).formula)
					.getFormulas();
			formulas.addFormula(cardFormula);
		}

		// generate info for supertypes
		generateSuperToAtomicMappings();

		// generate info for subsets of subtypes and supertypes of atomic types
		generateSubsetMappings();

		// generate info for fileds
		generateFieldMappings();

	}

	/**
	 * Returns a list of Decls, each representing one possible atomic product
	 * type
	 * 
	 * The idea is that a VarCreator passes in its Decls object, and this method
	 * returns a list of Decls objects, each of which the atomizer associates
	 * with a new VarCreator.
	 * 
	 */
	private List generateAtomizedDecls(Decls decls_) {

		List declsList = new ArrayList();

		// the number of Decl's in each Decls
		int declsLength = decls_.numChildren();

		// the approach is the following: move the index forward from 0 to
		// declsLength-1 and
		// for each index, select one possible atomized Decl and put it in the
		// current local scope
		// so that the mapping can be used for subsequent Decl's in the same
		// Decls that refer to
		// this quantified var.

		// _curLocalScope will be used during the atomization of multiplicity
		// expressions in declarations
		// it will be overwritten for each atomized decl and restored at the end
		// of this method.

		LocalScope scopeBackup = transientState._curLocalScope;

		// create a new scope here that points to the actual current scope. This
		// is done because
		// the helper procedure will make new local scopes sibilings of
		// _curLocalScope so you want
		// to ensure it includes everything up to this point.
		LocalScope newScope = new LocalScope();
		newScope.addParent(transientState._curLocalScope);
		transientState._curLocalScope = newScope;

		Decls newDecls = new Decls(decls_.getLocation());
		generateAtomizedDeclsHelper(declsList, decls_, newDecls, 0);

		// restore _curLocalScope
		transientState._curLocalScope = scopeBackup;

		return declsList;

	}

	/**
	 * 
	 * @param declsList
	 *            The running list containing the atomized Decls objects
	 * @param origDecls
	 *            The original Decls
	 * @param newDecls
	 *            The Decls currently being generated
	 * @param index
	 *            The index (0-based) of the next Decl in origDecls that has to
	 *            be considered.
	 */
	private void generateAtomizedDeclsHelper(List declsList, Decls origDecls,
			Decls newDecls, int index) {

		// check if newDecls is of the right size. If so, add this Decls
		if (index == origDecls.numChildren()) {
			declsList.add(newDecls);
			return;
		}

		// atomize the Decl expr at the current index, and recurse for each
		// possible atomic term

		Decl originalDecl = (Decl) origDecls.childAt(index);

		MultiplicityExpr multExpr = originalDecl.getExpr();

		List relTypes = atomizeType(multExpr.getType());

		if (relTypes.size() > 1) {
			if (multExpr instanceof SetMultExpr) {
				Multiplicity mult = ((SetMultExpr) multExpr).getMult();
				if (mult.equals(Multiplicity.SET)
						|| mult.equals(Multiplicity.LONE)
						|| mult.equals(Multiplicity.SOME)) {
					Dbg.user(new Msg(
							"Cannot use higher-order quantifiers on unions of more than one atomic type: "
									+ relTypes, origDecls.getParent()));
				}
			}
		}

		// boolean isArrowMult = multExpr instanceof ArrowMultExpr;

		Iterator multExprIter = new MultExprTermsIterator(multExpr, this);
		Variables vars = originalDecl.getVariables();
		Dbg.chk(vars.numChildren() == 1,
				"Atomization error: decl has more than one variable "
						+ originalDecl);
		while (multExprIter.hasNext()) {

			MultiplicityExpr newMultExpr = (MultiplicityExpr) multExprIter
					.next();

			// make a copy of newDecls to work with to have a new Decls for each
			// term
			Decls curDecls = (Decls) newDecls.copy();

			// set qualifiers
			Qualifiers qualifiers = new Qualifiers(originalDecl.getLocation());
			if (originalDecl.isDisj()) {
				if (originalDecl.isExh()) {
					qualifiers.addQualifier(Qualifier.PART);
				} else {
					qualifiers.addQualifier(Qualifier.DISJ);
				}
			} else if (originalDecl.isExh()) {
				qualifiers.addQualifier(Qualifier.EXH);
			}

			// generate a new copy of the variables
			Variables newVars = (Variables) vars.copy();

			Decl newDecl = new Decl(originalDecl.getLocation(),
					(Qualifiers) qualifiers, newVars, newMultExpr);

			curDecls.addDecl(newDecl);

			// generate a new localscope -- this will be undone after all the
			// decls are generated.

			LocalScope newScope = LocalScope.genScopeFromDecls(curDecls);

			if (transientState._curLocalScope != null) {
				for (Iterator parents = transientState._curLocalScope
						.getParents(); parents.hasNext();) {
					newScope.addParent((LocalScope) parents.next());
				}
			}

			transientState._curLocalScope = newScope;

			generateAtomizedDeclsHelper(declsList, origDecls, curDecls,
					index + 1);

		}

		/*
		 * // atomize the expr of the Decl using the current scope. assumes
		 * toExpr() returns a copy // which is currently the case SigmaExpr
		 * sigmaExpr = (SigmaExpr) multExpr.toExpr().applyReturnVisitor(this);
		 * 
		 * Variables vars = originalDecl.getVariables();
		 * Dbg.chk(vars.numChildren() == 1, "Atomization error: decl has more
		 * than one variable " + originalDecl);
		 * 
		 * for (Iterator termIter = sigmaExpr.getTerms().iterator();
		 * termIter.hasNext();) {
		 *  // recurse using this term Expr currentTerm = (Expr)
		 * termIter.next();
		 *  // make a copy of newDecls to work with to have a new Decls for each
		 * term Decls curDecls = (Decls) newDecls.copy();
		 *  // set qualifiers Qualifiers qualifiers = new
		 * Qualifiers(originalDecl.getLocation()); if (originalDecl.isDisj()) {
		 * if (originalDecl.isExh()) { qualifiers.addQualifier(Qualifier.PART); }
		 * else { qualifiers.addQualifier(Qualifier.DISJ); } } else if
		 * (originalDecl.isExh()) { qualifiers.addQualifier(Qualifier.EXH); }
		 *  // generate a new copy of the variables Variables newVars =
		 * (Variables) vars.copy();
		 * 
		 * MultiplicityExpr newMultExpr = new
		 * SetMultExpr(multExpr.getLocation(), (Multiplicity) ((SetMultExpr)
		 * multExpr).getMult().copy(), (Expr) currentTerm.copy());
		 * newMultExpr.setType(currentTerm.getType()); Decl newDecl = new
		 * Decl(originalDecl.getLocation(), (Qualifiers) qualifiers, newVars,
		 * newMultExpr);
		 * 
		 * curDecls.addDecl(newDecl);
		 *  // generate a new localscope -- this will be undone after all the
		 * decls are generated.
		 * 
		 * LocalScope newScope = LocalScope.genScopeFromDecls(curDecls);
		 * 
		 * if (_curLocalScope != null) { for (Iterator parents =
		 * _curLocalScope.getParents(); parents.hasNext();) {
		 * newScope.addParent((LocalScope) parents.next()); } }
		 * 
		 * _curLocalScope = newScope;
		 * 
		 * generateAtomizedDeclsHelper(declsList, origDecls, curDecls, index +
		 * 1); }
		 */

	}

	/**
	 * BUGGY old version (bug when the multiplicity expression of a Decl refers
	 * to a quantified variables defined in an earlier Decl of the same Decls)
	 * 
	 * @param decls_
	 * @return
	 */
	private List generateAtomizedDeclsOld(Decls decls_) {

		// a list of Decls, where each Decls is a complete set of declarations
		// for
		// the original decls_, and together the Decls cover the space covered
		// by
		// decls_
		List declsList = new ArrayList();

		// a list of declGroup's -- each declGroup is a List that contains Lists
		// of Decl's.
		// the intent is for the final part of the method to pick one list of
		// Decl's from
		// each declGroup to form a single Decls entry in declsList. Each
		// original
		// Decl in decls_ generates one declGroup
		List listOfDeclGroups = new ArrayList();

		for (Iterator declIter = decls_.getDeclIter(); declIter.hasNext();) {

			Decl decl = (Decl) declIter.next();

			// a list of atomized Decl's generated from one original Decl
			List declGroup = new ArrayList();
			listOfDeclGroups.add(declGroup);

			MultiplicityExpr multExpr = decl.getExpr();

			List relTypes = atomizeType(multExpr.getType());

			if (relTypes.size() > 1) {
				if (multExpr instanceof SetMultExpr) {
					Multiplicity mult = ((SetMultExpr) multExpr).getMult();
					if (mult.equals(Multiplicity.SET)
							|| mult.equals(Multiplicity.LONE)
							|| mult.equals(Multiplicity.SOME)) {
						Dbg.user(new Msg(
								"Cannot use higher-order quantifiers on unions of more than one atomic type: "
										+ relTypes, decls_.getParent()));
						// declsList.add(decls_);
					}
				}
			}

			boolean isArrowMult = multExpr instanceof ArrowMultExpr;

			// break up the expr

			SigmaExpr sigmaExpr = (SigmaExpr) multExpr.toExpr()
					.applyReturnVisitor(this);

			Variables vars = decl.getVariables();
			int numberOfVars = vars.numChildren();
			Dbg.chk(numberOfVars == 1);

			// a list whose elements are the same. Each element is a list of
			// Expr's (specifically, a term
			// from SigmaExpr). Used as "columns" for the increment()
			// function. Used to generate the decls in declGroup.
			// if numberOfVars is 1, then the list is just the terms from
			// the sigma expr.
			List exprsList = new ArrayList(numberOfVars);

			List exprs = new ArrayList(sigmaExpr.getTerms());
			for (int i = 0; i < numberOfVars; i++) {
				exprsList.add(exprs);
			}

			// generate the Decls objects to fill declsList
			int[] indices = new int[numberOfVars];
			// initialize indices
			for (int i = 0; i < indices.length; i++) {
				indices[i] = 0;
			}

			do {
				// for each iteration (set of indices--one per column), gather
				// into
				// batches by the term used (row referred to, basically). We do
				// that
				// so that if it was originally
				// set to be disj, we can do the same here
				// Then, generate one list of decls from them (one for each
				// term)
				// finally add that list of decls (represent one possible
				// transformation
				// of one original decl in decls_) into the proper declGroup for
				// this
				// original decl.
				Map termToSetOfVarIndex = new LinkedHashMap();
				for (int i = 0; i < indices.length; i++) {
					Expr term = (Expr) ((List) exprsList.get(i))
							.get(indices[i]);
					Set temp = (Set) termToSetOfVarIndex.get(term);
					if (temp == null) {
						temp = new LinkedHashSet();
						termToSetOfVarIndex.put(term, temp);
					}
					temp.add(new Integer(i));
				}

				// List to add to declGroup.
				List declsForIndices = new ArrayList();

				// now generate one decl for each term, and put them together in
				// declsForIndices
				// and stick it onto current declGroup

				for (Iterator termsIter = termToSetOfVarIndex.keySet()
						.iterator(); termsIter.hasNext();) {
					Expr term = (Expr) termsIter.next();
					Set varIndices = (Set) termToSetOfVarIndex.get(term);

					// set qualifiers
					Qualifiers qualifiers = new Qualifiers(decl.getLocation());
					if (decl.isDisj() && varIndices.size() > 1) {
						if (decl.isExh()) {
							qualifiers.addQualifier(Qualifier.PART);
						} else {
							qualifiers.addQualifier(Qualifier.DISJ);
						}
					} else if (decl.isExh()) {
						qualifiers.addQualifier(Qualifier.EXH);
					}

					// get the variables
					Variables declVars = new Variables(decls_.getLocation());
					for (Iterator varIndexIter = varIndices.iterator(); varIndexIter
							.hasNext();) {
						int varIndex = ((Integer) varIndexIter.next())
								.intValue();
						// extract Variable
						Variable v = (Variable) vars.childAt(varIndex);
						declVars.addVariable(v);
					}

					if (isArrowMult) {
						Dbg.fail("ENCOUNTERED ARROW MULT DURING ATOMIZATION");
						/*******************************************************
						 * Comment by Emina: this should no longer be needed
						 * since all multiplicity exprs in decls should have
						 * become SetMultExpr by this point (I hope)
						 ******************************************************/
						// then the expr should still be a binary product expr
						/**
						 * Dbg.chk( term instanceof BinaryExpr &&
						 * ((BinaryExpr)term).getOp().equals(BinaryExprOp.RELATION),
						 * "Error while atomizing declaration: " + decl);
						 * MultiplicityExpr newMultExpr = new ArrowMultExpr(
						 * multExpr.getLocation(), (Expr)
						 * ((BinaryExpr)term).getLeft().copy(), (Multiplicity)
						 * ((ArrowMultExpr)multExpr).getLeftMult().copy(),
						 * (Multiplicity)
						 * ((ArrowMultExpr)multExpr).getRightMult().copy(),
						 * (Expr) ((BinaryExpr)term).getRight().copy());
						 * newMultExpr.setType(term.getType());
						 * 
						 * Decl newDecl = new Decl( decl.getLocation(),
						 * (Qualifiers)qualifiers, (Variables)declVars.copy(),
						 * newMultExpr); //Decls newDecls = new
						 * Decls(decls_.getLocation());
						 * //newDecls.addDecl(newDecl);
						 * //declsList.add(newDecls);
						 * 
						 * declsForIndices.add(newDecl);
						 */
					} else {
						MultiplicityExpr newMultExpr = new SetMultExpr(multExpr
								.getLocation(),
								(Multiplicity) ((SetMultExpr) multExpr)
										.getMult().copy(), (Expr) term.copy());
						newMultExpr.setType(term.getType());
						Decl newDecl = new Decl(decl.getLocation(),
								(Qualifiers) qualifiers, (Variables) declVars
										.copy(), newMultExpr);
						// Decls newDecls = new Decls(decls_.getLocation());
						// newDecls.addDecl(newDecl);
						// declsList.add(newDecls);

						declsForIndices.add(newDecl);
					}

				}

				declGroup.add(declsForIndices);

			} while (increment(indices, exprsList, indices.length - 1));

		}

		// generate the Decls objects to fill declsList
		int[] indices = new int[listOfDeclGroups.size()];
		// initialize indices
		for (int i = 0; i < indices.length; i++) {
			indices[i] = 0;
		}

		do {
			Decls curDecls = new Decls(decls_.getLocation());
			for (int i = 0; i < indices.length; i++) {
				List declsForInd = (List) ((List) listOfDeclGroups.get(i))
						.get(indices[i]);
				for (Iterator dfiIter = declsForInd.iterator(); dfiIter
						.hasNext();) {
					Decl d = (Decl) dfiIter.next();
					curDecls.addDecl(d);
				}
			}
			declsList.add(curDecls);
		} while (increment(indices, listOfDeclGroups, indices.length - 1));

		return declsList;
	}

	/**
	 * generates the mappings from fields to SigmaExpr's and puts them in
	 * _fieldIdToSigmaExpr. Creates mangled fields when necessary.
	 */
	private void generateFieldMappings() {

		// String -> [ RelationType -> Integer ]
		// keeps track of the atomized fields that have been created. Used to
		// check if
		// a mangled field name is needed. This kind of conflict occurs when A1
		// and A2
		// extends A, and A is the atomic type; if A1 and A2 each individually
		// had
		// a field r (of type A1->B and A2->B), then during atomization, both
		// r's
		// are lifted up to the same type A->B. Before there was no apparent
		// distinction between these two r's, but now one is called r$ (and if
		// there
		// is a third one, it'll be called r$$, etc...). This change does not
		// affect
		// correctness, or even sharing, though because the correct behavior is
		// to have seaprate LeafId's for the two, and this had already been
		// done.
		// The new change only serves to prevent violating the invariants posed
		// by
		// TranslatableASTVisitor.
		Map createdUnmangledFieldsMap = new LinkedHashMap();

		for (Iterator signaturesIter = AtomizationState.state._allSigs
				.iterator(); signaturesIter.hasNext();) {
			Signatures sigs = (Signatures) signaturesIter.next();
			for (Iterator sigIter = sigs.getSignatureIter(); sigIter.hasNext();) {
				Signature curSig = (Signature) sigIter.next();

				// get decl's for fields
				Iterator decls = curSig.getDecls().getDeclIter();

				while (decls.hasNext()) {

					Decl decl = (Decl) decls.next();

					MultiplicityExpr multExpr = decl.getExpr();
					Expr expr = multExpr.toExpr();
					UnionType firstColumn = curSig.getUnionType();
					List exprRelTypes = atomizeType(firstColumn.product(expr
							.getType()));

					// generate a complete set of VariableExpr's for each name
					// in the decl
					Variables vars = decl.getVariables();
					for (Iterator varIter = vars.getVariableIter(); varIter
							.hasNext();) {
						Variable curVar = (Variable) varIter.next();
						String varName = curVar.getId().nodeString();
						LeafId origId = curSig.getFieldLeafId(varName);
						Dbg.chk(origId);

						// an instance of the current variable's VariableExpr
						// for reverse mapping
						// info
						VariableExpr curVarExpr = new VariableExpr(curVar
								.getLocation(), curVar);
						curVarExpr.setType(curSig.getFieldType(varName));
						curVarExpr.setLeafId(origId);
						info._atomizedIdToOldLeafExpr.put(curVarExpr
								.getLeafId(), curVarExpr);

						if (exprRelTypes.size() == 1) {
							// the field is of a single atomic type

							// the default value for number of types a field
							// with the same name and type
							// has been created
							int timesUsedPreviously = 0;

							RelationType relType = (RelationType) exprRelTypes
									.get(0);

							// check the number of types a relation of this name
							// and type has been used
							Map typeToNum = (Map) createdUnmangledFieldsMap
									.get(varName);
							if (typeToNum == null) {
								// no field of this type with name varName has
								// been created previously.
								typeToNum = new LinkedHashMap();
								typeToNum.put(relType, new Integer(1));
								createdUnmangledFieldsMap.put(varName,
										typeToNum);

							} else {
								Integer num = (Integer) typeToNum.get(relType);
								if (num == null) {
									// no field of this type with name varName
									// has been created previously.
									num = new Integer(1);
								} else {
									// a field with the same type and name has
									// been created previously
									timesUsedPreviously = num.intValue();
									num = new Integer(timesUsedPreviously + 1);
								}

								// record the number of times
								typeToNum.put(relType, num);
							}

							StringBuffer newName = new StringBuffer(varName);
							for (int i = 0; i < timesUsedPreviously; i++) {
								newName.append(ATOMIZATION_SEPARATOR);
							}

							Variable newVar = new Variable(new Id(newName
									.toString()));
							VariableExpr newVarExpr = new VariableExpr(newVar);
							newVarExpr.setType(new UnionType(relType));
							newVarExpr.setLeafId(new LeafId());
							SigmaExpr replacement = new SigmaExpr(newVarExpr);
							info._atomizedIdToOldLeafExpr.put(newVarExpr
									.getLeafId(), curVarExpr);
							info._fieldIdToSigmaExpr.put(origId, replacement);

							continue;
						}

						Iterator typesIter = exprRelTypes.iterator();
						RelationType relType = (RelationType) typesIter.next();
						SigType firstColumnType = (SigType) relType
								.getBasicTypeAt(0);

						String newName = createMangledFieldName(varName,
								relType);

						// check if this variable has already been made
						// previously
						Signature firstColumnSig = firstColumnType
								.getSignature();
						Variable newVar = new Variable(firstColumnSig
								.getLocation(), new Id(newName), false);
						VariableExpr newVarExpr = new VariableExpr(newVar);
						newVarExpr.setType(new UnionType(relType));

						if (firstColumnSig.getFieldLeafId(newName) != null) {
							// just reuse this id then
							newVarExpr.setLeafId(firstColumnSig
									.getFieldLeafId(newName));
						} else {
							// add this new field to the Signature and
							// ModuleInfo
							LeafIdMap lim = firstColumnSig.getLeafIdMap();
							LeafId newId = new LeafId();
							lim.put(newName, newId);
							info._command.moduleInfo.addFieldSigMapping(
									newName, firstColumnSig);
							newVarExpr.setLeafId(newId);
						}
						info._atomizedIdToOldLeafExpr.put(newVarExpr
								.getLeafId(), curVarExpr);
						SigmaExpr replacement = new SigmaExpr(newVarExpr);

						while (typesIter.hasNext()) {
							relType = (RelationType) typesIter.next();
							firstColumnType = (SigType) relType
									.getBasicTypeAt(0);

							newName = createMangledFieldName(varName, relType);

							firstColumnSig = firstColumnType.getSignature();
							newVar = new Variable(new Id(newName));
							newVarExpr = new VariableExpr(newVar);
							newVarExpr.setType(new UnionType(relType));

							if (firstColumnSig.getFieldLeafId(newName) != null) {
								// just reuse this id then, means it was made in
								// a previous
								// command's atomization
								newVarExpr.setLeafId(firstColumnSig
										.getFieldLeafId(newName));
							} else {
								// add this new field to the Signature
								LeafIdMap lim = firstColumnSig.getLeafIdMap();
								LeafId newId = new LeafId();
								lim.put(newName, newId);
								info._command.moduleInfo.addFieldSigMapping(
										newName, firstColumnSig);
								newVarExpr.setLeafId(newId);
							}
							info._atomizedIdToOldLeafExpr.put(curVarExpr
									.getLeafId(), curVarExpr);
							info._atomizedIdToOldLeafExpr.put(newVarExpr
									.getLeafId(), curVarExpr);
							replacement.addTerm(newVarExpr);
						}
						info._fieldIdToSigmaExpr.put(origId, replacement);
					}
				}

			}
		}
	}

	/**
	 * Fills in the stringToType map. If it's determined that this map's not
	 * needed, then we should be able to remove this code. However, as of now,
	 * this class uses the map's values (the types) to create an
	 * AtomizationVisitor.ScopeInfo, which is simply a convenience data
	 * structure that relies on the invariant that all types appearing in
	 * stringToType are scoped.
	 */
	private void generateScopedStringToType() {
		Dbg.chk(SigType.getStringToType() == info._command.stringToType);
		Map dummy = SigType.getStringToType();
		ScopeInfo scopeInfo = new ScopeInfo(SigType.getStringToType());
		Iterator idIter = info._command.leafId2Scope.keySet().iterator();
		info._command.stringToType = new LinkedHashMap();

		while (idIter.hasNext()) {
			LeafId id = (LeafId) idIter.next();
			String name = scopeInfo.getScopedSigName(id);
			Map dummy2 = SigType.getStringToType();
			if (SigType.getSigTypeForString(name) == null) {
				Dbg.fail("no SigType for " + name);
			}
			info._command.stringToType.put(name, SigType
					.getSigTypeForString(name));
		}
	}

	/**
	 * Both subsets of subtypes (of atomic types) and unions of atomic types
	 * and/or union types need to be converted. The first requires a simple type
	 * change in the SigExpr. The second requires some breaking up
	 */
	private void generateSubsetMappings() {

		for (Iterator signaturesIter = AtomizationState.state._allSigs
				.iterator(); signaturesIter.hasNext();) {
			Signatures sigs = (Signatures) signaturesIter.next();
			for (Iterator sigIter = sigs.getSignatureIter(); sigIter.hasNext();) {
				Signature curSig = (Signature) sigIter.next();
				if (!curSig.isSubset()) {
					continue;
				}

				// maps the atomic types used in this subset to the List of
				// SigExpr's
				// representing its members of that type.
				Map atomicTypesUsedToExprs = new LinkedHashMap();

				for (Iterator subsetExprs = curSig.getSubsets()
						.getSigExprIter(); subsetExprs.hasNext();) {
					SigExpr curSigExpr = (SigExpr) subsetExprs.next();

					// IMPORTANT -- NOTE that curSigExpr can potentially have no
					// LeafId's.
					// FixLeafIdsVisitor will fix this.

					SigType curType = (SigType) ((RelationType) curSigExpr
							.getType().getTypeIter().next()).getBasicTypeAt(0);

					if (info._atomicTypes.contains(curType)) {

						SigExprs curExprs = (SigExprs) atomicTypesUsedToExprs
								.get(curType);
						if (curExprs == null) {
							curExprs = new SigExprs();
							atomicTypesUsedToExprs.put(curType, curExprs);
							curExprs.addSigExpr(curSigExpr);
						} else {
							curExprs.addSigExpr(curSigExpr);
						}
					} else {
						if (info._superToAtomic.containsKey(curType)) {
							Set curAtomicTypes = (Set) info._superToAtomic
									.get(curType);

							for (Iterator atomicIter = curAtomicTypes
									.iterator(); atomicIter.hasNext();) {
								SigType curAtomicType = (SigType) atomicIter
										.next();
								SigExprs curExprs = (SigExprs) atomicTypesUsedToExprs
										.get(curAtomicType);
								if (curExprs == null) {
									curExprs = new SigExprs();
									atomicTypesUsedToExprs.put(curAtomicType,
											curExprs);
									SigExpr sigExpr = (SigExpr) curAtomicType
											.toExpr();
									sigExpr.setLeafId(curAtomicType
											.getSignature().getLeafId());
									curExprs.addSigExpr(sigExpr);

								} else {
									curExprs.addSigExpr(curSigExpr);
								}
							}
						} else if (info._subToAtomic.containsKey(curType)) {
							SigType curAtomicType = (SigType) info._subToAtomic
									.get(curType);
							SigExprs curExprs = (SigExprs) atomicTypesUsedToExprs
									.get(curAtomicType);
							if (curExprs == null) {
								curExprs = new SigExprs();
								atomicTypesUsedToExprs.put(curAtomicType,
										curExprs);
								curExprs.addSigExpr(curSigExpr);
							} else {
								curExprs.addSigExpr(curSigExpr);
							}
						} else {
							Dbg
									.fail("error determining atomic type for signature: "
											+ curType);
						}
					}

				}

				if (atomicTypesUsedToExprs.keySet().size() > 0) {
					/*
					 * the subset was on a supertype (of an atomic type). We
					 * will partition the subset into expression of only atomic
					 * types and create mappings. The newly generated subsets
					 * will have mangled names. Note that even if the supertype
					 * only had one atomic subtype, we still generate a mangled
					 * name because the code is systematic.
					 */

					// create the replacement SigmaExpr
					SigmaExpr replacement = null;

					// create new subsets, each of one atomic type

					for (Iterator atomicIter = atomicTypesUsedToExprs.keySet()
							.iterator(); atomicIter.hasNext();) {

						SigType curAtomic = (SigType) atomicIter.next();

						String subsetSigName = curSig.getName().getId()
								.nodeString()
								+ ATOMIZATION_SEPARATOR + curAtomic.toString();

						QualifiedName name = new QualifiedName(new Id(curSig
								.getLocation(), subsetSigName), curSig
								.getName().getPath());

						SigExprs xtends = new SigExprs();
						SigExprs subsetOf = (SigExprs) atomicTypesUsedToExprs
								.get(curAtomic);

						// how to solve the problem for the parameter for
						// static?
						Signature subsetSig = new Signature(curSig
								.getLocation(), name, xtends, subsetOf,
								new Decls(), new Fact(new QualifiedName(Id
										.generateId("Fact"), name.getPath())),
								Multiplicity.NONE, curSig.isProduct(), curSig
										.isAbstract());
						// need a LeafIdMap?
						subsetSig.setUnionType(new UnionType(new RelationType(
								curAtomic)));
						subsetSig.setParent(curSig.getParent());
						subsetSig.setLeafId(new LeafId());
						subsetSig
								.annotate("subset created during atomization for the set: "
										+ curSig);

						info._atomizedIdToOldLeafExpr.put(
								subsetSig.getLeafId(),
								/* temp == null ? */
								curSig.toSigExpr()); // : temp);

						// append to the SigmaExpr
						if (replacement == null) {
							SigExpr sigExpr = subsetSig.toSigExpr();
							sigExpr.setLeafId(subsetSig.getLeafId());
							replacement = new SigmaExpr(sigExpr);
						} else {
							SigExpr sigExpr = subsetSig.toSigExpr();
							sigExpr.setLeafId(subsetSig.getLeafId());
							replacement.addTerm(sigExpr);
						}

					}

					Dbg.chk(replacement, "error while atomizing subset: "
							+ curSig);

					// map original to itself
					info._atomizedIdToOldLeafExpr.put(curSig.getLeafId(),
							curSig.toSigExpr());

					info._sigIdToSigmaExpr.put(curSig.getLeafId(), replacement);

				}

			}
		}
	}

	/**
	 * generates mappings from supertypes to sets of atomic types that partition
	 * them in _superToAtomic. Also creates mappings in _sigIDToSigmaExpr
	 * 
	 */
	private void generateSuperToAtomicMappings() {
		// start from the atomic types, and go up
		for (Iterator atomicIter = info._atomicTypes.iterator(); atomicIter
				.hasNext();) {
			SigType atomic = (SigType) atomicIter.next();
			SigType superType = atomic.getSuperType();
			while (superType != null) {
				Set setAtomic = (Set) info._superToAtomic.get(superType);
				if (setAtomic == null) {
					setAtomic = new LinkedHashSet();
					info._superToAtomic.put(superType, setAtomic);
				}
				setAtomic.add(atomic);
				superType = superType.getSuperType();
			}
		}

		// use the info we just made to genereate replacement SigExpr mappings
		for (Iterator superIter = info._superToAtomic.keySet().iterator(); superIter
				.hasNext();) {
			SigType superType = (SigType) superIter.next();
			Iterator atomicIter = ((Set) info._superToAtomic.get(superType))
					.iterator();
			Dbg.chk(atomicIter.hasNext());
			SigType curAtomic = (SigType) atomicIter.next();
			SigmaExpr replacement = new SigmaExpr(curAtomic.getSignature()
					.toSigExpr());
			UnionType type = new UnionType(new RelationType(curAtomic));
			replacement.setType(type);

			while (atomicIter.hasNext()) {
				curAtomic = (SigType) atomicIter.next();
				replacement.addTerm(curAtomic.getSignature().toSigExpr());
				replacement.setType(replacement.getType().union(
						new UnionType(new RelationType(curAtomic))));
			}

			// put in the correct LeafID
			// replacement.applyVisitor(_command.sliv);

			// add mapping
			Dbg.chk(superType.getSignature().getLeafId(),
					"leafID of supertype is null while attempting to make SigExpr replacement: "
							+ superType);
			info._sigIdToSigmaExpr.put(superType.getSignature().getLeafId(),
					replacement);

		}
	}

	// ************************************************************
	// functions for determining how to atomize special things
	// as they're encountered
	// ************************************************************

	/**
	 * Used to handle variables generated from skolemization. Break them up into
	 * the sum of atomized versions of the variable if needed (and put it in the
	 * varIDToSigmaExpr map for future reference). Returns a sigma expression
	 * (even if no splitting up was done)
	 */
	private SigmaExpr generateVarMappings(VariableExpr varExpr_) {
		UnionType origType = varExpr_.getType();
		List atomizedRelTypes = atomizeType(origType);
		// System.out.println("---10------->>>> "+varExpr_);
		info._atomizedIdToOldLeafExpr.put(varExpr_.getLeafId(), varExpr_);

		if (atomizedRelTypes.size() > 1) {
			// need to break it up

			Iterator typesIter = atomizedRelTypes.iterator();

			List terms = new ArrayList();

			while (typesIter.hasNext()) {
				RelationType relType = (RelationType) typesIter.next();
				String newName = createMangledFieldName(varExpr_.getVar()
						.getId().nodeString(), relType);

				Variable newVar = new Variable(new Id(newName));
				VariableExpr newVarExpr = new VariableExpr(newVar);
				newVarExpr.setType(new UnionType(relType));
				newVarExpr.setLeafId(new LeafId());

				// record this skolem in command's skolemIds set, skolemType
				// map, and skolemLeafIdMap
				try {
					((FindCommand) info._command).skolemIds.add(newVarExpr
							.getLeafId());
					((FindCommand) info._command).skolemTypes.put(newName,
							newVarExpr.getType());
					info._command.skolemMap
							.put(newName, newVarExpr.getLeafId());
				} catch (Exception e) {
					Set newSet = new LinkedHashSet(
							((FindCommand) info._command).skolemIds);
					newSet.add(newVarExpr.getLeafId());
					((FindCommand) info._command).skolemIds = newSet;
				}

				terms.add(newVarExpr);
				info._atomizedIdToOldLeafExpr.put(newVarExpr.getLeafId(),
						varExpr_);
			}

			SigmaExpr ret = new SigmaExpr(terms);
			// create mapping
			info._varIdToSigmaExpr.put(varExpr_.getLeafId(), ret);
			return ret;
		} else {
			// make sure the type is set to the atomized type. e.g. you could
			// have a case
			// where foo is of type A1 but the atomized type is of type A, but
			// we can't
			// just return foo without resetting its type to A.
			varExpr_.setType(new UnionType((RelationType) atomizedRelTypes
					.get(0)));

			SigmaExpr ret = new SigmaExpr(varExpr_);
			// create mapping
			info._varIdToSigmaExpr.put(varExpr_.getLeafId(), ret);
			return ret;
		}

	}

	private BasicType getFirstBasicType(UnionType type) {
		RelationType firstRelType = (RelationType) type.getTypeIter().next();
		return firstRelType.getBasicTypeAt(0);
	}

	/**
	 * Given a type (e.g. A->A), returns the iden of that type (e.g. iden[A->A])
	 */
	private IdentityExpr getIdenExpr(RelationType type) {
		Dbg.chk(type, "tried to create a iden expr with null type");
		IdentityExpr retExpr = new IdentityExpr(new EmptyExpr());
		retExpr.setType(new UnionType(type));
		return retExpr;
	}

	/**
	 * Atomizes iden. e.g. If the atomic types are A and B, returns iden[A+A] +
	 * iden[B->B]
	 */
	private SigmaExpr getIdenReplacement() {
		// IMPORTANT
		// Note that this method can produce SigExpr with null LeafId's due
		// to the user of RelationType.toExpr()

		Iterator atomicIter = info._atomicTypes.iterator();

		List terms = new ArrayList();

		while (atomicIter.hasNext()) {
			SigType curAtomic = (SigType) atomicIter.next();
			List typeList = new ArrayList();
			typeList.add(curAtomic);
			typeList.add(curAtomic);
			RelationType type = new RelationType(typeList);
			Expr curTerm = getIdenExpr(type);
			curTerm.setType(new UnionType(type));
			Expr typeExpr = type.toExpr();
			curTerm = typeExpr.intersect(curTerm);
			terms.add(curTerm);
		}

		SigmaExpr retExpr = new SigmaExpr(terms);

		return retExpr;
	}

	/**
	 * Returns a none expression given a type.
	 */
	static EmptySetExpr getNoneExpr(RelationType type) {
		Dbg.chk(type, "tried to create a none expr with null type");
		EmptySetExpr retExpr = new EmptySetExpr(new EmptyExpr());
		retExpr.setType(new UnionType(type));
		return retExpr;
	}

	/**
	 * Creates a none expression of the desired arity. This is done by returning
	 * an atomized version of none[univ_1->univ_2->univ_n] where n is the
	 * desired arity.
	 */
	private SigmaExpr getNoneSigmaExpr(int arity) {

		UnionType _univType = new UnionType();

		for (Iterator atomicIter = info._atomicTypes.iterator(); atomicIter
				.hasNext();) {
			SigType curAtomic = (SigType) atomicIter.next();
			RelationType relType = new RelationType(curAtomic);
			_univType = _univType.union(new UnionType(relType));
		}

		return getNoneSigmaExpr(_univType, arity);

	}

	/**
	 * Creates a none expression on the given type for the desired arity. e.g.,
	 * running this method on the type A with arity 2 will return none[A->A]
	 */
	private SigmaExpr getNoneSigmaExpr(UnionType type, int arity) {

		UnionType origType = type;
		while (arity > 1) {
			type = type.product(origType);
			arity--;
		}

		List relTypes = atomizeType(type);
		List terms = new ArrayList();

		for (Iterator typeIter = relTypes.iterator(); typeIter.hasNext();) {
			EmptySetExpr retExpr = new EmptySetExpr(new EmptyExpr());
			RelationType curType = (RelationType) typeIter.next();
			retExpr.setType(new UnionType(curType));
			terms.add(retExpr);
		}

		SigmaExpr retExpr = new SigmaExpr(terms);

		return retExpr;
	}

	/**
	 * gets the scope of a SigType
	 * 
	 * @param type
	 * @return -1 if no scope is set
	 */
	private int getScope(SigType type) {
		Integer scope = (Integer) info._command.leafId2Scope.get(type
				.getSignature().getLeafId());
		if (scope == null) {
			Multiplicity mult = type.getSignature().getMult();
			if (mult.equals(Multiplicity.LONE) || mult.equals(Multiplicity.ONE)) {
				return 1;
			}

		}
		return (scope != null ? scope.intValue() : -1);
	}

	/**
	 * Atomizes univ into the union of all atomic types.
	 */
	private SigmaExpr getUnivReplacement() {
		Iterator atomicIter = info._atomicTypes.iterator();

		List terms = new ArrayList();

		while (atomicIter.hasNext()) {
			SigType curAtomic = (SigType) atomicIter.next();
			/*
			 * // univ = univ[A]+univ[B]+... Expr curTerm = new
			 * UniversalExpr(new EmptyExpr()); curTerm.setType(new UnionType(new
			 * RelationType(curAtomic)));
			 */

			// univ = A + B + ...
			Expr curTerm = curAtomic.getSignature().toSigExpr();
			terms.add(curTerm);
		}

		SigmaExpr retExpr = new SigmaExpr(terms);

		return retExpr;
	}

	/**
	 * utility function used whenever we have several lists and want to get all
	 * the possible combinations
	 */
	private boolean increment(int[] indices, List columns, int changeAt) {
		if (indices[changeAt] == ((List) columns.get(changeAt)).size() - 1) {
			indices[changeAt] = 0;
			if (changeAt == 0) {
				return false;
			} else {
				return increment(indices, columns, changeAt - 1);
			}
		} else {
			indices[changeAt] += 1;
			return true;
		}
	}

	/**
	 * If an atomic type had subtypes, this method creates mappings that map
	 * from sig expressions of those subtypes to equivalent forms that only
	 * utilize the atomic type.
	 * 
	 * e.g. suppose you have A2 extending A1 extending A, and A was the atomic
	 * type (the argument supertype for this procedure), A1 and A2 become
	 * subsets of type A, but we need not generate additional constraints about
	 * A2 being a subset of A1 because those were already done prior to
	 * atomization and are in the ast.
	 * 
	 * We do, however, need to add a <= cardinality constraint to reflect the
	 * scoping information, if it was available for the subtype. If the
	 * subtype's scope was exact, however, this step is skipped because an =
	 * cardinality constraint would have already been generated prior to
	 * atomization, and we'll atomize that later on.
	 */
	private void makeSubtypesSubsets(SigType supertype) {

		// iterate over all the scoped types, and add the set cardinality
		// constraint
		// for all exactly set scopes and their children (i.e. saying "run show
		// for 3
		// but exactly 4 A, 2 A1" will treat "2 A1" as "exactly 2 A1" if A1 is a
		// subtype of A

		makeSubtypesSubsetsHelper(supertype, supertype);

	}

	private void makeSubtypesSubsetsHelper(SigType atomicAncestor,
			SigType current) {

		for (Iterator subIter = current.getSubTypes().iterator(); subIter
				.hasNext();) {
			SigType sub = (SigType) subIter.next();

			Signature curSig = current.getSignature();
			Signature subsig = sub.getSignature();

			info._subToAtomic.put(sub, atomicAncestor);

			SigExpr newSigExpr = new SigExpr(subsig.getLocation(), subsig
					.getName());
			newSigExpr.setType(new UnionType(new RelationType(atomicAncestor)));
			// put in the correct LeafID
			newSigExpr.setLeafId(new LeafId());

			SigmaExpr replacement = new SigmaExpr(newSigExpr);

			// add mapping
			Dbg.chk(sub.getSignature().getLeafId(),
					"leafID of subtype is null while attempting to convert to subset: "
							+ sub);
			info._sigIdToSigmaExpr.put(sub.getSignature().getLeafId(),
					replacement);

			// check for remainder types, e.g. you have A whose remainder type
			// is A$, but
			// A$ is being made into a subset. You want the subset A$ to point
			// back to
			// A, not the subtype A$
			LeafExpr temp = (LeafExpr) info._atomizedIdToOldLeafExpr.get(subsig
					.toSigExpr().getLeafId());
			info._atomizedIdToOldLeafExpr.put(newSigExpr.getLeafId(),
					temp == null ? subsig.toSigExpr() : temp);

			TypeScope typescope = (TypeScope) info._sigTypeToTypeScope.get(sub);
			if (typescope == null) {
				// do nothin'
			} else {
				Formula cardFormula;
				if (typescope.isExact()) {
					// expression already generated before when exact, visitor
					// will take care of trasnforming the SigExpr

				} else {
					cardFormula = new ElemIntFormula(new CardinalityExpr(
							replacement), IntCompOp.INT_LTE,
							new LiteralIntExpr(typescope.getBound()));
					Formulas formulas = ((FormulaSeq) ((FindCommand) info._command).formula)
							.getFormulas();
					formulas.addFormula(cardFormula);
				}
			}

			makeSubtypesSubsetsHelper(atomicAncestor, sub);
		}
	}

	/**
	 * simple method for making type atomic. This involves: (1) creating an
	 * entry in _sigIdToSigmaExpr, (2) adding this type to the set of atomic
	 * types, and (3) turning any subtypes of this type into subsets.
	 */
	private void makeTypeAtomic(SigType type) {
		// when making a type atomic, add a mapping from its LeafId to a
		// SigmaExpr
		// enclosing a SigExpr of that type (this is done for uniformity, and
		// also because overloading can modify the type of a SigExpr A to B+C,
		// and the atomizer would be confused if it stays that way.
		info._sigIdToSigmaExpr.put(type.getSignature().getLeafId(),
				new SigmaExpr(type.getSignature().toSigExpr()));
		info._atomicTypes.add(type);
		makeSubtypesSubsets(type);
	}

	/**
	 * Replaces the previous setup() method, that was only used on new AVs.
	 * 
	 * @param info
	 */
	public AtomizationVisitor(final FindCommand command) {
		super();
		this.info = AtomizationState.state
				.getAtomizationInfo(command);
		Dbg.chk(this.info != null);
		transientState = new TransientState();

		// _allSigs = info._allSigs;
		// _atomizedIdToOldLeafExpr = info._atomizedIdToOldLeafExpr;
		// _atomicTypes = info._atomicTypes;
		// _superToAtomic = info._superToAtomic;
		// _subToAtomic = info._subToAtomic;
		// _sigTypeToTypeScope = info._sigTypeToTypeScope;
		// _sigIdToSigmaExpr = info._sigIdToSigmaExpr;
		// _fieldIdToSigmaExpr = info._fieldIdToSigmaExpr;
		// _varIdToSigmaExpr = info._varIdToSigmaExpr;
		// _curModuleInfo = info._curModuleInfo;
		// _fliv = info._fliv;
		// _createdStringToType = info._createdStringToType;
	}

	/**
	 * Strategy:
	 * 
	 * (1) re-initializes state variables (2) backs up and creates a new
	 * stringToType map (3) determines atomic types, creating remainder types
	 * and filling in all the relevant LeafIdMaps (4) applies this visitor to
	 * the formula of the command (5) applies FixLeafIdsVisitor (6) saves state
	 */
	public Object visit(final FindCommand command_) {

		// info = new AtomizationInfo(command_);
		// AtomCompilationState.globalState._commandToAtomizationInfo.put(command_,
		// info);
		Dbg.chk(info == AtomizationState.state
				.getAtomizationInfo(command_));
		transientState = new TransientState();

		Map stringToTypeBackup = SigType.getStringToType();
		SigType.setStringToType(info._command.stringToType);

		// System.out.println(((FindCommand)_command).formula.nodeString());
		// System.out.println(((FindCommand)command_).formula.pp());

		try {
			// this may not be the most elegant way to do it, but the purpose of
			// the 25-millisecond
			// wait is to ensure that the "Executing command..." message printed
			// by the main GUI
			// thread is printed before the info messaged below by the execution
			// thread.
			Thread.sleep(25);
		} catch (InterruptedException ie) {
			Dbg.fatal("fatal error");
		}
		Dbg.info("Atomizing command " + command_);
		long start = System.currentTimeMillis();
		// extract info from the signature declarations
		determineAtomicTypesAndRelations();

		// use the info to transform the formula
		command_.formula = (Formula) (command_.formula)
				.applyReturnVisitor(this);
		command_.formula.setParent(command_);

		// System.out.println(System.currentTimeMillis()-time);

		// generate a stringToType map (in the command) that corresponds to
		// the atomized model
		generateScopedStringToType();

		// clean up command
		command_.formula.applyReturnVisitor(new CanonicalizeFormulasVisitor());

		// set (and correct) LeafId's so that transl will work
		(command_.formula).applyVisitor(info._fliv);

		// reset map for later use by other commands
		SigType.setStringToType(stringToTypeBackup);

		if (DEBUG) {
			command_.formula.applyVisitor(new AtomizationCheckVisitor(info));
			consolePrintResults();
		}

		// put atomization info for this command inside the command
		AtomizationState.state._atomizedCommands.add(command_);
		long end = System.currentTimeMillis();
		Dbg.info("Finished atomization (" + ((end - start) / 1000.00) + "s)");

		return command_;
	}

	public Object visit(RunCommand runCommand_) {
		return visit((FindCommand) runCommand_);
	}

	public Object visit(CheckCommand checkCommand_) {
		return visit((FindCommand) checkCommand_);
	}

	/*----------------------------------------
	 * ENSIGMA (or "sigma-ize") OPERATIONS
	 * 
	 * Each of these methods takes an expression and returns a SigmaExpr
	 * 
	 * Several things to keep in mind:
	 * (1) when you create a new node, remember to set its type and location before returning it.
	 * (2) the LeafId's of any new leaves can generally be left unset until fliv is applied at the 
	 * end of atomization.
	 * (3) be careful not to use duplicate leaves because transl can only handle trees
	 *---------------------------------------*/

	public Object visit(Expr expr_) {
		Dbg.fail("unexpected expr: " + expr_);
		return expr_;
	}

	public Object visit(SigExpr sigExpr_) {
		LeafId id = sigExpr_.getLeafId();
		Dbg.chk(id, "sigExpr id was null when visited: " + sigExpr_);
		Dbg.chk(info._sigIdToSigmaExpr.containsKey(id),
				"sigExpr is not mapped " + sigExpr_);

		SigmaExpr retSigmaExpr = (SigmaExpr) ((SigmaExpr) info._sigIdToSigmaExpr
				.get(id)).copy();

		return retSigmaExpr;
	}

	public Object visit(EmptySetExpr noneExpr_) {
		return getNoneSigmaExpr(noneExpr_.getType().arity());
	}

	public Object visit(SigmaExpr sigmaExpr_) {
		return sigmaExpr_;
	}

	public Object visit(IdentityExpr idenExpr_) {
		return getIdenReplacement();
	}

	public Object visit(UniversalExpr univExpr_) {
		return getUnivReplacement();
	}

	/**
	 * Visits a VariableExpr. There are various cases:
	 * 
	 * <pre>
	 *  (1) varExpr_ is a field
	 *  (2) varExpr_ is a skolem whose mapping is known
	 *  (3) varExpr_ is a quantified variable we created
	 *  (4) varExpr_ is a newly encountered skolem
	 * </pre>
	 */
	public Object visit(VariableExpr varExpr_) {
		LeafId id = varExpr_.getLeafId();

		if (info._fieldIdToSigmaExpr.containsKey(id)) {
			return ((SigmaExpr) info._fieldIdToSigmaExpr.get(id)).copy();
		}

		if (info._varIdToSigmaExpr.containsKey(id)) {
			return ((SigmaExpr) info._varIdToSigmaExpr.get(id)).copy();
		}

		if (varExpr_.isQuantified && transientState._curLocalScope != null) {
			// look up type from scope
			UnionType type = transientState._curLocalScope.lookupType(varExpr_
					.nodeString());
			if (type != null) {
				varExpr_.setType(type);
			}
			SigmaExpr ret = new SigmaExpr(varExpr_);
			// System.out.println(" from curlocalscope: " + varExpr_ + "->" +
			// type);
			return ret;
		}

		/*
		 * I'm assuming that once it reaches this stage it was a dummy variable
		 * created from skolemization, and we need to make sure it's only of
		 * atomic types
		 */
		SigmaExpr replacement = generateVarMappings(varExpr_);

		return replacement;

	}

	/**
	 * <pre>
	 *  REF_TRANS_CLOSURE: convert to iden + &circ;, and visit that
	 *  TRANS_CLOSURE: besure that expr has only one atomic type, atomize expr.
	 *  TRANSPOSE: distribute &tilde; operator
	 * </pre>
	 */
	public Object visit(UnaryExpr unaryExpr_) {
		visit((Node) unaryExpr_);

		if (unaryExpr_.getExpr() instanceof EmptySetExpr) {
			return unaryExpr_.getExpr();
		}

		SigmaExpr expr = (SigmaExpr) unaryExpr_.getExpr();
		SigmaExpr retSigmaExpr = null;
		UnaryExprOp op = unaryExpr_.getOp();

		if (op.equals(UnaryExprOp.REF_TRANS_CLOSURE)) {
			// replace with iden+^(expr), and visit that
			Expr transClosure = new UnaryExpr(unaryExpr_.getLocation(),
					UnaryExprOp.TRANS_CLOSURE, unaryExpr_.getExpr());
			transClosure.setType(unaryExpr_.getType());
			Expr desugaredExpr = getIdenReplacement().union(transClosure);
			return desugaredExpr.applyReturnVisitor(this);
		}

		else if (op.equals(UnaryExprOp.TRANS_CLOSURE)) {
			// check if the expr is of only one atomic RelationType
			// this invariant should be true because atomic types are determined
			// with it
			// in mind (w/ "closedTypes" from the type checker)
			if (expr.getTypes().size() == 1) {
				RelationType firstType = (RelationType) expr.getTypes()
						.iterator().next();
				Dbg.chk(firstType.arity() == 2);
				Dbg.chk(firstType.getBasicTypeAt(0).equals(
						firstType.getBasicTypeAt(1)));

				// then allow atomization to do its thing (it might have to
				// convert some
				// subtypes into subsets, but in the end it'll only be of one
				// type)
				SigmaExpr atomizedExpr = (SigmaExpr) expr
						.applyReturnVisitor(this);
				Expr newRel = (Expr) atomizedExpr.getTerms().iterator().next();

				// use the expr as the new relation for which ^ is computed
				UnaryExpr curUnaryExpr = new UnaryExpr(
						unaryExpr_.getLocation(), op, newRel);
				curUnaryExpr.setType(newRel.getType());
				retSigmaExpr = new SigmaExpr(curUnaryExpr);
			} else {
				// this used to throw an exception here, which was a bad
				// assumption.
				// the user could have done something like ^(A->A + B->B), and
				// we
				// want to support that. so the correct thing to do here is to
				// pick out all the atomic types of form T->T.
				//
				// furthermore, if we have something like ^(A->A + A->B), where
				// A and B are atomic, we want this to mean ^(A->A) + A->B

				for (Iterator typeIter = expr.getTypes().iterator(); typeIter
						.hasNext();) {
					RelationType curType = (RelationType) typeIter.next();
					// should be binary no matter what
					Dbg.chk(curType.arity() == 2);

					Expr curExpr = (Expr) expr.getTerm(curType);

					// check if of form T->T
					if (curType.getBasicTypeAt(0).equals(
							curType.getBasicTypeAt(1))) {
						// use the expr as the new relation for which ^ is
						// computed
						UnaryExpr curUnaryExpr = new UnaryExpr(unaryExpr_
								.getLocation(), op, curExpr);
						curUnaryExpr.setType(curExpr.getType());
						if (retSigmaExpr == null) {
							retSigmaExpr = new SigmaExpr(curUnaryExpr);
						} else {
							retSigmaExpr.addTerm(curUnaryExpr);
						}
					} else {
						// if not just add the relation w/o putting ^
						if (retSigmaExpr == null) {
							retSigmaExpr = new SigmaExpr(curExpr);
						} else {
							retSigmaExpr.addTerm(curExpr);
						}
					}
				}

				Dbg.chk(retSigmaExpr,
						"transitive closure not properly atomized.");
			}
		}

		else if (op.equals(UnaryExprOp.TRANSPOSE)) {
			Iterator termsIter = expr.getTerms().iterator();
			Dbg.chk(termsIter.hasNext(),
					"transpose expression has empty expr: " + unaryExpr_);

			List newTerms = new LinkedList();

			while (termsIter.hasNext()) {
				Expr term = (Expr) termsIter.next();
				Expr newTerm = new UnaryExpr(term.getLocation(),
						UnaryExprOp.TRANSPOSE, term);
				newTerm.setType(term.getType().transpose());
				newTerms.add(newTerm);
			}
			retSigmaExpr = new SigmaExpr(newTerms);
		} else {
			Dbg.fail("Unknown unary expr operator during atomization: "
					+ unaryExpr_);
		}

		return retSigmaExpr != null ? retSigmaExpr : (Expr) unaryExpr_;
	}

	/**
	 * Atomizes binary expressions. The supported types of expressions are:
	 * union, diff, intersect, join (. : and []), relation domain restrictions
	 * are not supported because they should have been desugared prior to
	 * atomization
	 */
	public Object visit(BinaryExpr binExpr_) {
		visit((Node) binExpr_);
		SigmaExpr leftExpr = (SigmaExpr) binExpr_.getLeft();
		SigmaExpr rightExpr = (SigmaExpr) binExpr_.getRight();
		SigmaExpr retSigmaExpr;
		BinaryExprOp op = binExpr_.getOp();

		if (op.equals(BinaryExprOp.UNION)) {
			List retTypes = new ArrayList();
			Set leftTypesCopy = new LinkedHashSet(leftExpr.getTypes());
			leftTypesCopy.addAll(rightExpr.getTypes());
			Iterator typesIter = leftTypesCopy.iterator();

			if (!typesIter.hasNext()) {
				// empty expr
				return getNoneSigmaExpr(leftExpr.getType().arity());
			}

			while (typesIter.hasNext()) {
				RelationType relType = (RelationType) typesIter.next();
				Expr newLeftExpr = leftExpr.getTerm(relType);
				Expr newRightExpr = rightExpr.getTerm(relType);

				Expr newExpr;

				// if a type only appears on one side (left/right), simply keep
				// that one term for unions
				if (newLeftExpr == null) {
					newExpr = newRightExpr;
					// continue;
				} else if (newRightExpr == null) {
					newExpr = newLeftExpr;
				} else {
					newExpr = new BinaryExpr(binExpr_.getLocation(),
							newLeftExpr, binExpr_.getOp(), newRightExpr);
				}
				newExpr.setType(new UnionType(relType));
				retTypes.add(newExpr);
			}
			retSigmaExpr = new SigmaExpr(retTypes);
		} else if (op.equals(BinaryExprOp.DIFF)) {
			/*
			 * Notes: if a certain type appears only on the left side, then the
			 * returned SigmaExpr. contains the left expr for that type. If a
			 * certain type appears only on the right side, we ignore it.
			 * 
			 * Hence, if A1, A2, B1, and C1 are expression of type A, A, B, C,
			 * then: (A1+B1)-(A2+C1) is atomized to (A1-A2)+B1
			 */
			List retTypes = new ArrayList();
			Set leftTypesCopy = new LinkedHashSet(leftExpr.getTypes());
			leftTypesCopy.addAll(rightExpr.getTypes());
			Iterator typesIter = leftTypesCopy.iterator();

			if (!typesIter.hasNext()) {
				// empty expr
				return getNoneSigmaExpr(leftExpr.getType().arity());
			}

			while (typesIter.hasNext()) {
				RelationType relType = (RelationType) typesIter.next();
				Expr newLeftExpr = leftExpr.getTerm(relType);
				Expr newRightExpr = rightExpr.getTerm(relType);

				Expr newExpr;

				if (newLeftExpr == null) {
					// no corresponding term on the left, don't need to include
					// this type
					// for difference
					continue;
				} else if (newRightExpr == null) {
					// if there's no corresponding term on the right, just
					// include the
					// term on the left
					newExpr = newLeftExpr;
				} else {
					newExpr = new BinaryExpr(binExpr_.getLocation(),
							newLeftExpr, binExpr_.getOp(), newRightExpr);
				}
				newExpr.setType(new UnionType(relType));
				retTypes.add(newExpr);
			}
			retSigmaExpr = new SigmaExpr(retTypes);
		} else if (op.equals(BinaryExprOp.INTERSECT)) {
			/*
			 * Notes: only the intersected types between the left and right
			 * expressions are looked at.
			 */

			Iterator typesIter = leftExpr.getIntersectedTypes(rightExpr)
					.iterator();

			if (!typesIter.hasNext()) {
				// empty expr
				return getNoneSigmaExpr(leftExpr.getType().arity());
			}

			List retTypes = new ArrayList();

			while (typesIter.hasNext()) {
				RelationType relType = (RelationType) typesIter.next();
				Expr newExpr = new BinaryExpr(binExpr_.getLocation(), leftExpr
						.getTerm(relType), binExpr_.getOp(), rightExpr
						.getTerm(relType));
				newExpr.setType(new UnionType(relType));
				retTypes.add(newExpr);
			}
			retSigmaExpr = new SigmaExpr(retTypes);
		} else if (op.equals(BinaryExprOp.JOIN_DOT)
				|| op.equals(BinaryExprOp.JOIN_DOUBLECOLON)
				|| op.equals(BinaryExprOp.JOIN_SQBRACKETS)) {

			// map used to keep track of the new terms created. At the end, a
			// SigmaExpr is created from this map.
			Map unionTypeToSigmaTerm = new LinkedHashMap();

			// iterate across the ending column types of the leftExpr
			for (Iterator leftEndIter = leftExpr.getLastColumnTypes()
					.iterator(); leftEndIter.hasNext();) {
				BasicType basType = (BasicType) leftEndIter.next();

				// see if there're any join-able terms at the right
				if (rightExpr.containsFirstColumnType(basType)) {
					for (Iterator rightJoinableTerms = rightExpr
							.getTermsWithFirstColumn(basType).iterator(); rightJoinableTerms
							.hasNext();) {
						Expr curRightTerm = (Expr) rightJoinableTerms.next();

						// create products between left and right terms
						for (Iterator leftTerms = leftExpr
								.getTermsWithLastColumn(basType).iterator(); leftTerms
								.hasNext();) {
							Expr curLeftTerm = (Expr) leftTerms.next();
							BinaryExpr newBinaryTerm = new BinaryExpr(binExpr_
									.getLocation(),
									(Expr) (curLeftTerm).copy(), binExpr_
											.getOp(), (Expr) (curRightTerm)
											.copy());
							newBinaryTerm.setType(curLeftTerm.getType().join(
									curRightTerm.getType()));

							// record this new term.
							if (unionTypeToSigmaTerm.containsKey(newBinaryTerm
									.getType())) {
								Expr expr = (Expr) unionTypeToSigmaTerm
										.get(newBinaryTerm.getType());
								expr = expr.union(newBinaryTerm);
								unionTypeToSigmaTerm.put(newBinaryTerm
										.getType(), expr);
							} else {
								unionTypeToSigmaTerm.put(newBinaryTerm
										.getType(), newBinaryTerm);
							}
						}
					}
				}

			}

			if (unionTypeToSigmaTerm.isEmpty()) {
				return getNoneSigmaExpr(leftExpr.getType().arity()
						+ rightExpr.getType().arity() - 2);
			}

			retSigmaExpr = new SigmaExpr(new ArrayList(unionTypeToSigmaTerm
					.values()));
		}

		else if (op.equals(BinaryExprOp.RELATION)) {
			Iterator leftTermsIter = leftExpr.getTerms().iterator();
			Iterator rightTermsIter = rightExpr.getTerms().iterator();

			List retTypes = new ArrayList();

			while (leftTermsIter.hasNext()) {
				Expr curLeftTerm = (Expr) leftTermsIter.next();
				for (rightTermsIter = rightExpr.getTerms().iterator(); rightTermsIter
						.hasNext();) {
					Expr curRightTerm = (Expr) rightTermsIter.next();

					Expr left = (Expr) ((Expr) curLeftTerm).copy();
					Expr right = (Expr) ((Expr) curRightTerm).copy();
					Expr newProductExpr = new BinaryExpr(left,
							BinaryExprOp.RELATION, right);
					newProductExpr.setType(left.getType().product(
							right.getType()));
					// shouldn't need to manually atomize the type here
					retTypes.add(newProductExpr);
				}
			}
			retSigmaExpr = new SigmaExpr(retTypes);
		} else {
			retSigmaExpr = null;
			Dbg.fail("Atomization doesn't process BinaryExpr with op: "
					+ binExpr_.getOp());
		}

		return retSigmaExpr;

	}

	/**
	 * Atomizes if-then-else expressions. First atomizes the formula, and the
	 * then/else expressions. Then group terms in then and else expressions
	 * according to type, and create a separate if-then-else expr (with the same
	 * formula) for each type. Finally, returns the union of these if-then-else
	 * expr's.
	 * 
	 * Hence, "if f(x) then (A+B1) else (B2+C)" (B1 and B2 are both of type B)
	 * becomes: "if f(x) then A else none[A] + if f(x) then B1 else B2 + if f(x)
	 * then none[C] else C"
	 */
	public Object visit(IfThenElseExpr ifExpr_) {
		visit((Node) ifExpr_);

		Formula formula = ifExpr_.getIfFormula();
		SigmaExpr thenExpr = (SigmaExpr) ifExpr_.getThenExpr();
		SigmaExpr elseExpr = (SigmaExpr) ifExpr_.getElseExpr();

		List retTypes = new ArrayList();

		Iterator thenTypes = thenExpr.getTypes().iterator();
		while (thenTypes.hasNext()) {
			RelationType curType = (RelationType) thenTypes.next();

			Expr newExpr;
			if (elseExpr.containsType(curType)) {
				newExpr = new IfThenElseExpr(ifExpr_.getLocation(), formula,
						thenExpr.getTerm(curType), elseExpr.getTerm(curType));
				newExpr.setType(new UnionType(curType));
			} else {
				newExpr = new IfThenElseExpr(ifExpr_.getLocation(), formula,
						thenExpr.getTerm(curType), getNoneExpr(curType));
				newExpr.setType(new UnionType(curType));
			}

			retTypes.add(newExpr);
		}

		// now do the types in the else expression that weren't in the then expr
		for (Iterator elseTypes = elseExpr.getTypes().iterator(); elseTypes
				.hasNext();) {
			RelationType curType = (RelationType) elseTypes.next();
			if (!thenExpr.containsType(curType)) {
				// we haven't made one for this type yet
				Expr newExpr = new IfThenElseExpr(ifExpr_.getLocation(),
						formula, getNoneExpr(curType), elseExpr
								.getTerm(curType));
				newExpr.setType(new UnionType(curType));
				retTypes.add(newExpr);
			}

		}

		SigmaExpr retExpr = new SigmaExpr(retTypes);

		return retExpr;

	}

	/**
	 * Atomizes a ComprehensionExpr by taking its Decls and generating multiple
	 * sets of Decls such that each is atomic but together they partition all
	 * the possibilities implied by the original Decls. Then, creates a
	 * ComprehensionExpr for each new Decls and adds the ComprehensionExpr
	 * together as a SigmaExpr.
	 */
	public Object visit(ComprehensionExpr compExpr_) {
		compExpr_.setDecls(separateVarCreatorDecls(compExpr_));

		// set scopes
		visit((VarCreator) compExpr_);

		// backup these fields
		final LocalScope _oldLocalScopeToRm = transientState._localScopeToRemove;
		final LocalScope _oldLocalScopeToAdd = transientState._localScopeToAdd;
		final LocalScope _oldCurLocalScope = transientState._curLocalScope;

		// get the groups of atomized Decls
		final List atomizedDeclsList = generateAtomizedDecls(compExpr_
				.getDecls());

		final Iterator declsIter = atomizedDeclsList.iterator();
		Dbg.chk(declsIter.hasNext(), "empty atomized Decls in compExpr: "
				+ compExpr_);

		// terms of the SigmaExpr
		List terms = new ArrayList();

		// do the same for all the other Decls
		final String backupCurQuantVarName = transientState._innermostQuantifiedVarName;
		final Variable backupCurQuantVar = transientState._innermostQuantifiedVar;

		while (declsIter.hasNext()) {
			Decls curDecls = (Decls) declsIter.next();

			// get the UnionType associated with this Decls
			List basTypes = new ArrayList();

			Decl curDecl = null;

			for (Iterator decls = curDecls.getDeclIter(); decls.hasNext();) {
				curDecl = (Decl) decls.next();
				basTypes.add(getFirstBasicType(curDecl.getExpr().getType()));
			}
			Dbg.chk(curDecl, "generated no decls from " + compExpr_);
			transientState._innermostQuantifiedVar = (Variable) curDecl
					.getVariables().getVariableIter().next();
			transientState._innermostQuantifiedVarName = transientState._innermostQuantifiedVar
					.getId().nodeString();

			UnionType curType = new UnionType(new RelationType(basTypes));

			// generate a new localscope
			LocalScope oldScope = compExpr_.getLocalScope();
			LocalScope newScope = LocalScope.genScopeFromDecls(curDecls);

			for (Iterator parents = oldScope.getParents(); parents.hasNext();) {
				newScope.addParent((LocalScope) parents.next());
			}

			transientState._localScopeToRemove = oldScope;
			transientState._localScopeToAdd = newScope;
			transientState._curLocalScope = newScope;

			final ComprehensionExpr newCompExpr = new ComprehensionExpr(
					compExpr_.getLocation(), curDecls, (Formula) compExpr_
							.getFormula().copy(), false);
			// newCompExpr.setLeafIdMap(compExpr_.getLeafIdMap());
			newCompExpr.setType(curType);
			newCompExpr.setLocalScope(newScope);

			final Formula returnedFormula = (Formula) newCompExpr.getFormula()
					.applyReturnVisitor(this);
			newCompExpr.setFormula(returnedFormula);

			terms.add(newCompExpr);

		}

		transientState._innermostQuantifiedVar = backupCurQuantVar;
		transientState._innermostQuantifiedVarName = backupCurQuantVarName;

		// restore info for other VarCreators of the same depth
		transientState._localScopeToRemove = _oldLocalScopeToRm;
		transientState._localScopeToAdd = _oldLocalScopeToAdd;
		transientState._curLocalScope = _oldCurLocalScope;

		SigmaExpr sigmaExpr = new SigmaExpr(terms);

		return sigmaExpr;
	}

	/*----------------------------------------
	 * DESIGMA OPERATIONS
	 * 
	 * These methods atomize formulas or other nodes that may contain SigmaExpr into equivalent
	 * forms that do not use SigmaExpr or contain union types
	 *----------------------------------------*/

	/**
	 * Atomizes a cardinality expr. e.g., #(A+B) ---> #A + #B
	 */
	public Object visit(CardinalityExpr cardExpr_) {
		visit((Node) cardExpr_);

		SigmaExpr expr = (SigmaExpr) cardExpr_.getExpr();

		Iterator termsIter = expr.getTerms().iterator();

		Expr curTerm = (Expr) termsIter.next();
		IntExpr curSum = new CardinalityExpr(cardExpr_.getLocation(), curTerm);

		while (termsIter.hasNext()) {
			curTerm = (Expr) termsIter.next();
			curSum = new BinaryIntExpr(cardExpr_.getLocation(), curSum,
					IntExprOp.PLUS, new CardinalityExpr(
							cardExpr_.getLocation(), curTerm));
		}
		return curSum;

	}

	/**
	 * Atomizes an elementary formula. This is done by categorizing the left and
	 * right expr's into pairs by type, creating an elem formula for each pair,
	 * and conjuncted together. If a certain type only appears on one side, use
	 * an appropriate none expr for the pair.
	 * 
	 * There are a couple of special cases:
	 * 
	 * <pre>
	 *  (1) none in x --&gt; returns an EmptyFormula (always true)--this is cleaned up later on in 
	 *  CanonicalizeFormulasVisitor.
	 *  (2) x in y, where x and y's types do not intersect.  Normally, the typechecker would get rid
	 *  of all of these, so they must be intermediate forms generated during atomization.  In fact,
	 *  there are two possibilities: (a) the atomization of quantified formulae produced this 
	 *  inconsistent form, or (b) a subtle case with function arguments. e.g. foo is declared as type A 
	 *  (atomic subtypes A1 and A2), and you say something like foo in A2, even though you called the 
	 *  function with a set of type A1 for foo.  In both (a) and (b), we return a false formula.
	 * </pre>
	 */
	public Object visit(ElemFormula elemForm_) {
		visit((Node) elemForm_);

		Expr left = elemForm_.getLeft();
		Expr right = elemForm_.getRight();

		if (left instanceof EmptySetExpr && !elemForm_.getOp().isNegated()) {
			// none is in anything--this formula is meaningless
			return new EmptyFormula();
		}

		CompOp op = elemForm_.getOp();
		if (op.isNegated())
			op = op.negation();
		if (op.equals(CompOp.SUBSETCOLON))
			op = CompOp.SUBSETIN;

		if (right instanceof EmptySetExpr) {
			// it means all the sets described on the left are empty
			SigmaExpr leftExpr = (SigmaExpr) elemForm_.getLeft();
			Iterator termsIter = leftExpr.getTerms().iterator();
			Expr curTerm = (Expr) termsIter.next();
			EmptySetExpr correctNoneExpr = getNoneExpr(curTerm.getType()
					.toRelationType());

			Formula retFormula = new ElemFormula(elemForm_.getLocation(),
					curTerm, op, correctNoneExpr);

			while (termsIter.hasNext()) {
				curTerm = (Expr) termsIter.next();
				correctNoneExpr = getNoneExpr(curTerm.getType()
						.toRelationType());
				retFormula = retFormula.and(new ElemFormula(elemForm_
						.getLocation(), curTerm, op, correctNoneExpr));
			}

			if (elemForm_.getOp().isNegated()) {
				// negate the conjuncted formulae
				retFormula = retFormula.not();
			}

			return retFormula;
		}

		SigmaExpr leftExpr = (SigmaExpr) elemForm_.getLeft();
		SigmaExpr rightExpr = (SigmaExpr) elemForm_.getRight();

		Iterator typesIter = leftExpr.getIntersectedTypes(rightExpr).iterator();

		if (!typesIter.hasNext()) {

			// This happens in cases where quantifiers separate out unions of
			// atomic
			// types (so they are no longer in one SigmaExpr)--we should return
			// a false formula
			if (transientState._innermostQuantifiedVar != null) {
				VariableExpr varExpr = new VariableExpr(
						elemForm_.getLocation(),
						transientState._innermostQuantifiedVar);
				UnionType type = transientState._curLocalScope
						.lookupType(transientState._innermostQuantifiedVarName);
				varExpr.setType(type);
				return new ElemFormula(elemForm_.getLocation(), varExpr,
						elemForm_.getOp(), getNoneExpr(type.toRelationType()));
			} else {
				// a subtle case that happens when a function argument foo is
				// declared as type
				// A (atomic subtypes A1 and A2), and you say something like foo
				// in A2, even
				// though you called the function with a set of type A1 for foo.
				// in this case, just return a false formula signified by
				// negating the
				// EmptyFormula
				if (elemForm_.getOp().isNegated()) {
					return new EmptyFormula();
				} else {
					return new EmptyFormula().not();
				}
			}

		}

		List retTypes = new ArrayList();
		Set types = new LinkedHashSet(leftExpr.getTypes());
		types.addAll(rightExpr.getTypes());
		typesIter = types.iterator();

		Dbg.chk(typesIter.hasNext());

		Formulas formulas = new Formulas(elemForm_.getLocation());

		while (typesIter.hasNext()) {
			RelationType relType = (RelationType) typesIter.next();
			Expr newLeftExpr = leftExpr.getTerm(relType);
			Expr newRightExpr = rightExpr.getTerm(relType);

			if (newLeftExpr == null) {
				newLeftExpr = getNoneExpr(relType);
			}
			if (newRightExpr == null) {
				newRightExpr = getNoneExpr(relType);
			}

			formulas.addFormula(new ElemFormula(elemForm_.getLocation(),
					newLeftExpr, op, newRightExpr));

		}

		Formula retFormula = new FormulaSeq(elemForm_.getLocation(), formulas);
		if (elemForm_.getOp().isNegated()) {
			retFormula = retFormula.not();

			// System.out.println("e "+ (System.currentTimeMillis()-time));
		}
		return retFormula;
	}

	/**
	 * Atomizes quantified expressions. It is assumed that only LONE expressions
	 * will be encountered here, because NO and ONE quantified expressions are
	 * desugared prior to atomization.
	 * 
	 * An example: lone (A+B) ---> (lone A && no B) || (no A && no B)
	 */
	public Object visit(QuantifiedExpr quantExpr_) {
		// ensigma expr first
		visit((Node) quantExpr_);
		SigmaExpr expr = (SigmaExpr) quantExpr_.getExpr();
		Formula ret = quantExpr_;

		if (quantExpr_.getQuantifier().equals(Quantifier.LONE)) {
			/*
			 * There are three known ways to do this: (1) with cardinality
			 * expressions
			 * 
			 * (2) lone e1 && no e2 && no e3 && ... && no e_n || no e1 && lone
			 * e2 && no e3 && ... && no e_n ... || no e1 && no e2 && no e3 &&
			 * ... && lone e_n
			 * 
			 * (3) lone e1 && lone e2 && lone e3 && ... && lone e_n && (no e1 ||
			 * (no e2 && no e3 && ... && no e_n) && (no e2 || (no e3 && no e4 &&
			 * ... && no e_n) ... && (no e_n-1 || no e_n)
			 * 
			 * We initially tried (1), but it was quite inefficient. We replaced
			 * (1) with (2), which showed minor improvements, but we think (3)
			 * may be even better, because "you don't need to check each e_i
			 * against the e_j where j < i, so the clauses get shorter as you go
			 * down."
			 */

			// approach (3)
			List exprTermsList = new LinkedList(expr.getTerms(false));

			Formulas retForms = new Formulas(quantExpr_.getLocation());

			// generate first clause (lone e1 && lone e2 && ... && lone e_n)
			Formulas loneConjunctionForms = new Formulas(quantExpr_
					.getLocation());
			for (Iterator termsIter = exprTermsList.iterator(); termsIter
					.hasNext();) {
				Expr curTerm = (Expr) termsIter.next();
				Formula form = new QuantifiedExpr(quantExpr_.getLocation(),
						Quantifier.LONE, (Expr) curTerm.copy());
				loneConjunctionForms.addFormula(form);
			}
			FormulaSeq loneConjunction = new FormulaSeq(quantExpr_
					.getLocation(), loneConjunctionForms);
			retForms.addFormula(loneConjunction);

			// generate the next n-1 clauses
			for (int start = 0; start < exprTermsList.size() - 1; start++) {
				Expr startTerm = (Expr) exprTermsList.get(start);
				List restOfTerms = exprTermsList.subList(start + 1,
						exprTermsList.size());

				// generate (no e_start)
				Expr noneTerm = getNoneExpr(startTerm.getType()
						.toRelationType());
				Formula startForm = new ElemFormula(quantExpr_.getLocation(),
						(Expr) startTerm.copy(), CompOp.SUBSETIN, noneTerm);

				// generate (no e_start+1 && no e_start+2 && ... && no e_n)
				Formulas restForms = new Formulas(quantExpr_.getLocation());
				for (Iterator restIter = restOfTerms.iterator(); restIter
						.hasNext();) {
					Expr curTerm = (Expr) restIter.next();
					Expr curNoneTerm = getNoneExpr(curTerm.getType()
							.toRelationType());
					Formula curForm = new ElemFormula(quantExpr_.getLocation(),
							(Expr) curTerm.copy(), CompOp.SUBSETIN, curNoneTerm);
					restForms.addFormula(curForm);
				}
				FormulaSeq restForm = new FormulaSeq(quantExpr_.getLocation(),
						restForms);

				// take the disjunction of the two formulas above
				Formula curDisjunction = new BinaryFormula(quantExpr_
						.getLocation(), startForm, LogicOp.OR, restForm);

				// add this clause to the main conjunction
				retForms.addFormula(curDisjunction);

			}

			ret = new FormulaSeq(quantExpr_.getLocation(), retForms);
		} else {
			Dbg.fail("QuantifiedExpr not desugared before atomization: "
					+ quantExpr_);
		}
		return ret;
	}

	public Object visit(QuantifiedFormula quantForm_) {
		quantForm_.setDecls(separateVarCreatorDecls(quantForm_));

		// take care of parent scoping
		visit((VarCreator) quantForm_);

		// backup these fields
		final LocalScope _oldLocalScopeToRm = transientState._localScopeToRemove;
		final LocalScope _oldLocalScopeToAdd = transientState._localScopeToAdd;
		final LocalScope _oldCurLocalScope = transientState._curLocalScope;

		final Formulas formulas = new Formulas(quantForm_.getLocation());
		Formula retFormula = null;

		final List atomizedDecls = generateAtomizedDecls(quantForm_.getDecls());

		final String backupCurQuantVarName = transientState._innermostQuantifiedVarName;
		final Variable backupCurQuantVar = transientState._innermostQuantifiedVar;

		for (Iterator declsIter = atomizedDecls.iterator(); declsIter.hasNext();) {
			Decls curDecls = (Decls) declsIter.next();

			Decl firstDecl = (Decl) curDecls.getDeclIter().next();
			transientState._innermostQuantifiedVar = (Variable) firstDecl
					.getVariables().getVariableIter().next();
			transientState._innermostQuantifiedVarName = transientState._innermostQuantifiedVar
					.getId().nodeString();

			// generate a new localscope
			LocalScope oldScope = quantForm_.getLocalScope();
			// System.out.println(curDecls.getDeclIter().next());
			LocalScope newScope = LocalScope.genScopeFromDecls(curDecls);

			for (Iterator parents = oldScope.getParents(); parents.hasNext();) {
				newScope.addParent((LocalScope) parents.next());
			}

			transientState._localScopeToRemove = oldScope;
			transientState._localScopeToAdd = newScope;
			transientState._curLocalScope = newScope;

			Quantifier quant = quantForm_.getQuantifier();

			QuantifiedFormula newFormula = new QuantifiedFormula(quantForm_
					.getLocation(), quant, (Decls) curDecls.copy(),
					(Formula) quantForm_.getFormula().copy(), false);
			// false so that a new LocalScope won't be generated

			// note: apparently copy() was intentionally written to not copy the
			// LeafIdMap's
			// hence, due to the above copy() call, nested QuantifiedFormulas
			// have
			// null LeafIdMap's. These are now set appropriately by the
			// FixLeafIdsVisitor
			newFormula.setLocalScope(newScope);

			Formula returnedFormula = (Formula) newFormula.getFormula()
					.applyReturnVisitor(this);
			newFormula.setFormula(returnedFormula);

			if (retFormula == null) {
				retFormula = newFormula;
			} else {
				if (quantForm_.getQuantifier().equals(Quantifier.SOME)) {
					retFormula = retFormula.or(newFormula);
				} else if (quantForm_.getQuantifier().equals(Quantifier.ALL)) {
					retFormula = retFormula.and(newFormula);
				} else {
					Dbg.fatal("unexpected quantifier during atomization: "
							+ quantForm_.getQuantifier());
				}
			}
		}

		transientState._innermostQuantifiedVar = backupCurQuantVar;
		transientState._innermostQuantifiedVarName = backupCurQuantVarName;

		// restore info for other VarCreators of the same depth
		transientState._localScopeToRemove = _oldLocalScopeToRm;
		transientState._localScopeToAdd = _oldLocalScopeToAdd;
		transientState._curLocalScope = _oldCurLocalScope;

		return retFormula;
	}

	public Object visit(SumIntExpr sumIntExpr_) {
		sumIntExpr_.setDecls(separateVarCreatorDecls(sumIntExpr_));
		// set scopes
		visit((VarCreator) sumIntExpr_);

		// backup these fields
		LocalScope _oldLocalScopeToRm = transientState._localScopeToRemove;
		LocalScope _oldLocalScopeToAdd = transientState._localScopeToAdd;
		LocalScope _oldCurLocalScope = transientState._curLocalScope;

		// get the groups of atomized Decls
		List atomizedDeclsList = generateAtomizedDecls(sumIntExpr_.getDecls());

		Iterator declsIter = atomizedDeclsList.iterator();
		Dbg.chk(declsIter.hasNext(), "empty atomized Decls in sumIntExpr: "
				+ sumIntExpr_);

		// terms of the sum of SumIntExpr's
		List terms = new ArrayList();

		String backupCurQuantVarName = transientState._innermostQuantifiedVarName;
		Variable backupCurQuantVar = transientState._innermostQuantifiedVar;

		while (declsIter.hasNext()) {
			Decls curDecls = (Decls) declsIter.next();

			// get the UnionType associated with this Decls
			List basTypes = new ArrayList();

			Decl curDecl = null;

			for (Iterator decls = curDecls.getDeclIter(); decls.hasNext();) {
				curDecl = (Decl) decls.next();
				basTypes.add(getFirstBasicType(curDecl.getExpr().getType()));
			}
			Dbg.chk(curDecl, "generated no decls from " + sumIntExpr_);
			transientState._innermostQuantifiedVar = (Variable) curDecl
					.getVariables().getVariableIter().next();
			transientState._innermostQuantifiedVarName = transientState._innermostQuantifiedVar
					.getId().nodeString();

			UnionType curType = new UnionType(new RelationType(basTypes));

			// generate a new localscope
			LocalScope oldScope = sumIntExpr_.getLocalScope();
			LocalScope newScope = LocalScope.genScopeFromDecls(curDecls);

			for (Iterator parents = oldScope.getParents(); parents.hasNext();) {
				newScope.addParent((LocalScope) parents.next());
			}

			transientState._localScopeToRemove = oldScope;
			transientState._localScopeToAdd = newScope;
			transientState._curLocalScope = newScope;

			SumIntExpr newSumIntExpr = new SumIntExpr(
					sumIntExpr_.getLocation(), curDecls, (IntExpr) sumIntExpr_
							.getExpr().copy());
			// newSumIntExpr.setLeafIdMap(sumIntExpr_.getLeafIdMap());
			newSumIntExpr.setLocalScope(newScope);

			IntExpr returnedIntExpr = (IntExpr) newSumIntExpr.getExpr()
					.applyReturnVisitor(this);
			newSumIntExpr.setExpr(returnedIntExpr);

			terms.add(newSumIntExpr);

		}

		transientState._innermostQuantifiedVar = backupCurQuantVar;
		transientState._innermostQuantifiedVarName = backupCurQuantVarName;

		// restore info for other VarCreators of the same depth
		transientState._localScopeToRemove = _oldLocalScopeToRm;
		transientState._localScopeToAdd = _oldLocalScopeToAdd;
		transientState._curLocalScope = _oldCurLocalScope;

		Dbg.chk(!terms.isEmpty(), "no terms generated from sumintexpr: "
				+ sumIntExpr_);

		Iterator termsIter = terms.iterator();
		IntExpr intExpr = (IntExpr) termsIter.next();

		while (termsIter.hasNext()) {
			IntExprOp op = IntExprOp.PLUS;
			intExpr = new BinaryIntExpr(sumIntExpr_.getLocation(), intExpr, op,
					(IntExpr) termsIter.next());
		}

		return intExpr;
	}

	/*
	 * MISCELLANEOUS
	 */

	/**
	 * Sets the LocalScope correctly
	 */
	public Object visit(VarCreator varCreator_) {
		LocalScope scope = varCreator_.getLocalScope();

		for (Iterator scopeIter = scope.getParents(); scopeIter.hasNext();) {
			LocalScope parent = (LocalScope) scopeIter.next();
			if (parent == transientState._localScopeToRemove) {
				scopeIter.remove();
			}
		}
		if (transientState._localScopeToAdd != null) {
			scope.addParent(transientState._localScopeToAdd);
		}
		return varCreator_;
	}

	public Object visit(IntExprCastExpr castExpr_) {
		Dbg.fail("Should not see IntExprCastExpr");
		return castExpr_;
	}

	public Object visit(ExprCastIntExpr castExpr_) {

		// atomize expr
		visit((Node) castExpr_);

		// distribute "int" operator
		// could improve this code by filtering out non-Int terms, but this is
		// not currently done because I need to check w/ Emina to see whether
		// Int can have subtypes

		SigmaExpr expr = (SigmaExpr) castExpr_.getExpr();

		Iterator termsIter = expr.getTerms().iterator();

		Expr curTerm = (Expr) termsIter.next();
		IntExpr curSum = new ExprCastIntExpr(castExpr_.getLocation(), curTerm);

		while (termsIter.hasNext()) {

			curTerm = (Expr) termsIter.next();
			curSum = new BinaryIntExpr(castExpr_.getLocation(), curSum,
					IntExprOp.PLUS, new ExprCastIntExpr(
							castExpr_.getLocation(), curTerm));

		}

		return curSum;
	}

	/**
	 * Desugars the decls of a VarCreator such that there is only one variable
	 * per Decl.
	 * 
	 */
	private Decls separateVarCreatorDecls(VarCreator varCreator_) {
		Decls decls = varCreator_.getDecls();
		Decls newDecls = new Decls(decls.getLocation());

		for (Iterator declIter = decls.getDeclIter(); declIter.hasNext();) {
			Decl curDecl = (Decl) declIter.next();
			MultiplicityExpr multExpr = curDecl.getExpr();

			for (Iterator varIter = curDecl.getVariables().getVariableIter(); varIter
					.hasNext();) {
				Variable curVar = (Variable) varIter.next();
				Decl newDecl;
				newDecl = Decl.in(curVar, (MultiplicityExpr) multExpr.copy());
				newDecl.setLocation(curDecl.getLocation());
				newDecls.addDecl(newDecl);
			}
		}

		return newDecls;
	}

	
	public static void atomize(final FindCommand command_) {
    	// atomize the command here (JIT atomization)
		if (!AtomizationState.state._atomizedCommands.contains(command_)) {
			command_.applyReturnVisitor(new AtomizationVisitor(command_));
			AtomizationState.state._atomizedCommands.add(command_);
		}
	}
}
